(navigation image)
Home American Libraries | Canadian Libraries | Universal Library | Community Texts | Project Gutenberg | Children's Library | Biodiversity Heritage Library | Additional Collections
Search: Advanced Search
Anonymous User (login or join us)
See other formats

Full text of "mit :: lcs :: tr :: MIT-LCS-TR-136"


MAC TR-136 

Stephen A. Ward 

September 1974 

This research was supported by the Advanced 
Research Projects Agency of the Department 
of Defense under ARPA Order No. 2095 which 
was monitored by ONR Contract No. N00014- 



This empty page was substituted for a 
blank page in the original document. 


The author gratefully acknowledges the assistance of his Thesis Committee in 
this work. Professors Jack Dennis and Joseph Weizenbaum, his readers, 
provided helpful suggestions and encouragement during the course of the thesis 
research. The author feels a special indebtedness to his thesis supervisor, 
Professor Michael Dertouzos, for his essential contributions to the direction, 
motivation, and technical content of this work. 

Particular thanks are due the author's wife, Debbie, whose constant support 
and encouragement have thus far been rewarded by a depressingly long period as 
the wife of a student. 

The author is grateful to the Department of Electrical Engineering for the 
Instructorship under which much of this research was carried out. This work 
was also supported in part by Project MAC, an M.I.T. research program 
sponsored by the Advanced Research Projects Agency, Department of Defense, 
under Office of Naval Research Contract N00014-70-A-0362-GO06. 

This empty page was substituted for a 
blank page in the original document. 



The expressive power of a particular applicative language 
may be characterized by the set of abstract functions di- 
rectly representable in that language. The common FUNARG 
and applicative order problems are scrutinized in this 
way, and the effects of these weaknesses are 
inexpressibil ity of classes of functions. 

related to the 

Certain computable functions which are inexpressible in the 
lambda calculus are identified, and it is established that 
the interpretation of these functions requires a mechanism 
fundamentally equivalent to multiprocessing. The EITHER 
construct is proposed as an extension to the lambda calculus, 
and several theories including this mechanism are presented 
and proved consistent (in the sense that they introduce no 
new equivalences into the lambda calculus). 

conversi on , 
this adjunct 
normal forms in 

A syntactic analog to the Scott construction, 

is developed in conjunction with these theories; 

allows reduction of expressions having no 

the usual lambda calculus to finite normal form approximations 

of the expressions. This leads naturally to a technique for 

proving the extensional equivalence of lambda calculus 

expressions which are not interconvertible. 

title submitted 

*This report reproduces a thesis of the same 
to the Department of Electrical Engineering, Massachusetts 
Institute of Technology, in partial fulfillment of the 
requirements for the degree of Doctor of Philosophy, June 1974 


Table of Contents 

Table of Contents 


1.1: Programming Language Semantics 
Applicative Languages 
The Thesis: Statement of the Problem 
Outline of the Thesis 
Functional Domains 
1.5.1: Intuitive Criteria for Functions 
1.5.2: Functional Domain: Definition 


: Interpreter Structure and Expressive Power 
2.1: Syntax of Models 
2.2: Curried Functions 
2.3: The FUNARG Problem 

2.3.1: The S model 

2.3.2: Arithmetic Completeness of S 

2.3.3: Functional Incompleteness of S 
2.4: Evaluation Order 

2.4.1: The T Model 

2.4.2: Functional Incompleteness of T 
2.5: The N model 

2.5.1: Axioms for the Lambda Calculus 

2.5.2: Normal order: Substitution The M Evaluator Axiomatic Consistency of N 
2.6: Functional Domain of N 
2.7: Summary 

: Motivation for a Multi-valued Semantics 
3.1: Necessity of non- functions: WHICHFF 
3.2: Coding primitives: The C model 
3.2.1: The Turing-machine Tar Pit 
3.2.2: Functionality of DECODE LAMBDA-free AEs 
3.2,2.2: An Enumeration of D 
E model: Multiprocessing primitives 
The Intuitive Paradox 
Multi-valued Semantic Elements 
5.1: Domains of Specification 
5.2: EITHER and the Lambda Calculus 
The Power Set Domain 
Interpretation of F* 
3.8: Computable elements of F* 
3.9: Summary 




4: Theories of EITHER-conversion 

4.1: Preliminary Definitions 

4.2: The Either-R Theories 

4.2.1: Properties of Either Theories 
4.2.2: EITHER and Evaluation Order 
4.2.3: Consistency of Either-R 

4.3: Summary 

5: *-Conversion 

5.1: The R- # Theories 

5.1.1: Significance of normal forms 
5.1.2: Theorem on Normal Forms 
5.1.3: Relation to the Lambda Calculus 
5.1.4: Consistency of R-* Theories 

5.2: Applications to the Lambda Calculus 

5.3: Summary 

6: The Either-R-* Theories 

6.1: Consistency of Either-R-« 
6.2: Relation of » to EITHER 
6.3: Evaluators for E 
6.4: Summary 

:able of Contents 


7: The Either-K Theories 





K-abs traction 

Consistency of Either-K Theories 

Functional Domains of Either-K 


3: Summary and Conclusions 


i. 3 



Directions of Future Research 

9: References 

10: Biographical note 


1 10 
1 1 1 

1 1 
1 1 
1 17 


This empty page was substituted for a 
blank page in the original document. 


Chapter 1 : 

1.1: Programming Language Semantics . 

The semantics of a programming language may be viewed as a theory which 
accounts for the behavior of programs written in that lakngua^e. An,, 
interpreter for a language L is a model for the semantics .of L, and a language 
whose semantics is incomplete (in the sense of an incomplete theory) ,may have 
many "correct" interpreters which behave differently Just as an incomplete 
theory may have disparate models. We find that the usual more specific 
definitions of semantics (e.g. "the relation between expressions and the 
objects vhich they denote") make assumptions about the structure of a universe 
of "meanings" which are difficult to justify in the general case, where side 
effects, assignment, and transfers of ceotroli mast biPiee&unted for 
3emant Really. Such consideration* motivate the reattfeMon of the present ' 
work to applicative languages. 

Serious concern for formal semantics is not usually an important consideration 
in the architecture of practical languages. TypicaJ.lv, a language is designed, 
largely by pragmatic considerations and the formal statement of its semantics 
is either abandoned entirely or postponed until the more important 
implementation issues are sorted out. The subsequent semantic formalization 
of th* language inevitably becomes a major task, and the complexity, volume, 
and inscrutability of the result may constrain its "usefulness, A classic 
example of such an undertaking is the description of PL/1 in the Vienna 
Definition Language[ 24], 

An alternative technique of language design, exemplified to some extent in 
LISP[26] and its recent derivatives, Involves the specification of the 
pragmatics of a language after decisions on some particular concise semantics 
have been made. Unfortunately languages so designed tend to have serious 
defects from a practical point of view and are abandoned or complicated by the 
addition of aj. 1122. mechanisms to make them more useful. 



The designer of a language is thus confronted with a choice between concise 
semantics and practical usability, and he justifiably tends to opt for the 
latter alternative. The extent to which semantic considerations may be 
reconciled with practical issues remains an important open question, and the 
development of practical languages with concise, elegant semantics is the long 
term goal of much of Computer Science research. The problem is being attacked 
from two discernible directions: (i) semantic formalisms which deal with the 
mechanisms of extant practical languages, such as the analysis of 
uninterpreted schema ta[9, 8, 13, 17,25] ; and (ii) the adaptation of existing 
formalisms to very simple model languages such as the lambda 
calculus[2,3,5,15,22]. The work reported here falls naturally into the 
second category. 

1.2: Applicative Languages 

Familiar concepts of mathematics provide an informal semantics for many 
aspects of computer languages. Manuals for most programming languages relate 
various program constructs to such notions as real nu«b«rs, arithmetic, and 
functions, with which the reader is presumed to be acquainted. Often 
terminology and notation are borrowed from mathematics, implying some informal 
relation between, say, a FORTRAN "function" and the common mathematical notion 
of f met ion. This relation is only approximate, since for example no 
mathematical analog has been established for the FORTRAN function which prints 
its argument on the teletype. In order to formalize the relationship between 
program constructs and mathematical notions, then, we focus our attention on 
the highly restricted class of applicative languages. 

The semantic bases of applicative languages are the theories of mathematical 
functions, and the constructs of these languages are restricted to simple 
analogs of the related mathematical notions. Each applicative language 
provides a syntactic formalism for the representation of functions and their 
application to arguments, and the semantics of an applicative language is in 
general a rule for the association of expressions, constructed according to 
this formalism, with values from an abstract semantic domain containing 
functions and constants. Formalizing a consistent semantics for an 

1.2 -9- 

applicative language appears to be an easy first step in pursuing the general 
problem of programming language semantics; since set theory provides 
satisfactory semantic domains, all that remains is the seemingly simple 
association of expressions with set theoretic functions and constants. 

Yet even this simple problem is plagued with explications, add it is only in 
recent years that progress has been made in thin are* isKargely due to 
techniques developed by Dana ScottlS ,G*22h In tact, -tits' Usual set theoretic 
characterization of functions is not so well adapted to the semantics of 
applicative languages as one might suspect: type restrictions, placed on set 
theoretic functions in order to avoid Russel 's Paradox, are difficult to 
reconcile with the natural proclivity of applicative languages for the 
self-application of functions. The work of Scott justifies our optimism that 
such problems^ are traetabley and that the semantics ofs applicative languages 
may be based on the mathematics of functions. Th* extension of tha reciting 
semantics to non-applicative mechanisms such as assignment and side effects 
however, remains ah area of grave uncertainty, and it seems likely that 
theories of functions will ultimately prove to be inadequate bases for the 
semantics of programming languages in general. In the meantime, however, 
applicative languages and their fmctionnl aew^ie 4omaioa ; ape probably the 
closest we have cane to a successful programming language semantics, and we 
feel that there is much insight to be gained from further exploration of this 

The semantics of an„ applicative language L,thi6 t pajr bai^iewed as a mapping 
between the set of walfca expressions ia ; la (the djoto ^ 4iS2flittfiS. of h) and 
and a semantic detain of abatriot functions and osnntants. * -consequence of 
the Turing Universality of L is that this napping *uat 4w many to one; each 
abstract semantic element has, in general, infinitely many representations in 
the language L. The semantic mapping thus leads naturally to a notion of 
semantic equivalence between expressions in L, partitioning the domain of 
discourse of L into equivalence classes each of which corresponds to a single 
abstract semantic element. 

-10- 1.3 

1.3: The Thesis: Statement of the Problem 

The problem which this thesis addresses is the characterization of the 
expressive power of an applicative language in terms of the structure of its 
abstract semantic domain. This process generally involves relating specific 
applicative' language features to the expressibility of particular classes of 
functions, e.g. the solution of the FUHARG problem to the expressibility of 
functions mapping integers onto an infinite range of senantieally distinct 
functions. ■ ' -, 

This work focuses on a very few specific language mechanisms, with particular 
attention given to an applicative analog of multiprocessing. Partial answers 
are provided to such questions as: 

1) Are there functions whose computability depends fundamentally on a noti&n 
analogous to multiprocessing? 

2) What applicative mechanisms are necessary for the expression of such 
functions, and is the impact of these mechanisms on the structure of the 
semantic domain? 

3) What is such relationship between such multiprocessing constructs and 
other issue* of applicative language evaluation, such as evaluation 

The work presented here might be characterized as a search for an applicative 
language L which is ffunotlonallr complete in > the saaaalfehat every computable 
function definable on the semantic domain of L is expressible in L -- our 
reluctance. to cite this as the principal goal of the thesis is probably due to 
our failure to find such a language. 

1.4: Outline of the Thesis 

The organization of the remaining chapters is as follows: 

Chapter 2 develops the basic framework through the presentation of three 
interpreters for applicative languages, designated S (stack environment), 
T (tree environment), and N (normal order). Each interpreter exemplifies 

1.4 -11- 

a typical language limitation and each is- used to relate a specific 
language characteristic to the expressibility of a particular class of 

Chapter 3 demonstrates a particular computable function which is 

inexpressible both in N and in the lambda calculus, and relates this 
inexpressibility to the semantic requirement that an expression in these 
languages have at most a single value. Two alternative language 
extensions are discussed, each of which solves this- specific 
expressibility problem. The solutions involve, respectively, primitives 
for coding the representation of functions as integers and a 
multiprocessing primitive called EITHER. Each of these extensions 
requires modification of the structure of the semantic domain, with the 
use of coding leading to drastic and undesirable consequences. For this 
and related reasons, EITHER is chosen. To account for the semantics of 
EITHER, the semantic domain of N is expanded into a power set and each 
expression X is associated semantically with an enumerate le set containing 
the admissible values of X. 

The formalization of EITHER-augmented languages may procede in several ways, 
differing in the restrictions placed on evaluation order. Chapters 4, 5, 6, 
and 7 deal with certain formal theories, based on the lambda calculus, for the 
reduction of expressions involving the EITH2R construct: 

Chapter 4 provides basic definitions and presents the Either-R Theory, in 
which lambda conversion is allowed only in expressions whose arguments 
are in normal form. This restriction is motivated by the intuitive 
desire to maintain the distributivity of functions over terms of an 
EITHER clause, but it limits the power of languages based on this theory. 

Chapter 5 develops a theory of '-conversion, designed to mitigate the 

limitations imposed by the restricted lambda conversion of the Either-R 
Theory. The element • is introduced as a canonical representation of 
every nonterminating computation, and a syntactic mechanism is provided 
for the reduction of expressions to approximations which are in normal 
form. The use of •-conversion provides techniques for proving certain 
relationships in the conventional lambda calculus. This chapter presents 

-12- 1.H 

results which are of interest independently of their relation to the 
development of the Either theories. 

Chapter 6 presents the Either-R-« theory, combining the EITHER mechanism 
with "-conversion, and establishes its consistency. While this system 
retains the restriction on lambda conversion* it has the power of the 
lambda calculus augmented by the EITHER primitive. Thus, languages based 
on Either-fl-» solve the specific expressibility problem raised in Chapter 
3- Interpreters and semantics for such languages are discussed. 

Chapter 7 presents the Either-K theory, which combines the EITHER construct 
with unrestricted lambda conversion. Significant semantic differences 
between the Either-R and Either-K theories are noted, and it is 
informally observed that the removal of the restriction on lambda 
conversion leads to the expressibility of certain functions which are 
inexpressible in the Either-R-* languages. 

The last chapter summarizes the results of this work and proposes avenues for 
future research. 

1.5: Functional Domains 

An underlying assumption of this research is that the fundamental semantic 
intent of applicative languages is to provide computational models of 
mathematical functions. As a consequence of this assumption, we are inclined 
to view functions in an applicative language as approximations or models of 
abstract mathematical functions, and to treat any disparity between the 
behavior of the computationa'l model and the corresponding mathematical 
function as a "bug" or idiosyncrasy in the language. 

The thrust of this research is aimed at the limitations of particular 
applicative languages as models of systems of mathematical functions. We 
begin by specifying, in the next section, criteria which must be obeyed by 
applicative functions to be intuitively satisfactory as models of mathematical 
functions, and then distinguish for each applicative language L that subset of 
the domain of L containing only such intuitively satisfying functions. We 
call such a subdomain of L a functional domain of L. 

1.5.1: Intuitive Criteria for Functions 


^stricting our attention for the moment to unary (single argument) functions, 
vve note that 

1) A function £ is a ffiafifiifl* from a domain D f to a range R . The 
set-theoretic model of I is a set of ordered pairs, {. .fo r >. . . } , such 
that £[D 1 ]=R 1 if and only if KD^R^.i. an element of £. 

2) A function f may be partial over domain D, i.e., there may be elements D. 
in D such that fjD^ is undefined; this corresponds to the practical * 
situation of a nonterminal ing computation or "a computation which results 
in an error condition. We shall refer to such a computation as 

3) If f and g. provide the same mapping, then they are the same function. 

*0 & is a aiifcafiJL of £ (in the set-theoretic sense) if and only if for every 
D t in the domain of g., gj^^ implies fjD^aR . 

Given a language L and a function £, a principal intuitive requirement is the 
distinction between the function £ and the vario** algorithms (or expressions 
in L) which may be used to compute £. A ma joif SoAplicatlon in the semantics 
of applicative languages arises from this many-to-one correspondance between 
algorithms and functions, particularly in light of the well known 
un decidability of equivalences between algorithms. 

1.5.2: Functional Domain: Definition 

The intuitive considerations of the previous nation motivate the following 

Deffl 1,1: A iimciianai dfiBain F is a set containing the set M of natural 

numbers and computable functions, 1 along with an equivalence relation - 
such that: 

tvS^ff^? 6 ^ 10311 ^ 313 ^ 1 ' we sna11 use the term function with no implied 
no^C? 3 ^ 10 ^"?: thus Unctions include fun ctionaTsoriFbitrary order 
consistent with the typeless character of the applicative languages considered 

-14- 1.5.2 

1) if x is in N or i is in N, then x~y if and only if x=y. 

2) if neither x_ nor y_ is in N, then x~y if and only if for every z in 
F, 2lCs.1~Y.C2.] or both diverge together. 

3) if x~y_, then for every z_ in F, z_[xj~alvj of both diverge together. 

Clause (1) simply asserts that different numbers, eg 2 and 3, are semantically 
different objects. Clause (2) asserts that any object in F that is not a 
number is a function, and moreover that functions are semantically equivalent 
if and only if they perform equivalent computations for every set of 
arguments. Clause (3) insists that the application of a function to 
semantically equivalent arguments yield semantically equivalent values. 

An expression z, is said to be fuggtlonqj , over t;he domain F if, for every 
choice of x_ and y_ in F, x_~y_ implies that z_[xj~z_[yj or both computations 
diverge together. Thus (3) is the requirement that every function in a 
functional domain F be functional over F. 

We note that the equivalence relation ~ is not, in general, computable. 
Furthermore, there may be elements x. and y_ in F sueh that x.~y_ is not defined, 
that i£, such that neither x_~v_ nor ~(x.~y_) ;;. is derivable from the above 

This definition is rather more specific than necessary. The choice of natural 
numbers as a basis of semantically distinct constants, rather than, say, 
character strings or floating point numbers, is arbitrary. In dealing with 

the lambda calculus we could make the apparently stronger requirement that 
normal form expressions be semantically distinct, rather than just the 
particular normal form expressions whiqh are numeric constants; however it 
happens that the two alternatives are entirely equivalent in the context of 
our model languages, and our present definition is the less dependent on 
particular syntactic considerations. 

2 -15- 

Chapter 2: 
Interpreter Structure and Expressive Power 

In this chapter several illustrative interpreters for applicative languages 
are presented, and compromises in their implementation are related to the 
inexpressibility of certain functions. The model interpreters are taken from 
Dertouzos[3l where they are discussed and motivated in greater detail. 

2.1: Syntax of Models 

The essential components of an applicative language syntax are conventions for 
the representation and application of functions. Typical applicative 
languages provide for the representation of functions by either or" both of the 
following means: 

1) A set of reserved symbols designating w^ilUJtt' XtofitlflDl whose semantics 
are basic to the language; 

2) A convention for functional abstraction, or the definition of new 
functions by means of expressions containing variables. 

The pure lambda calculus of Church[i] is illustrative of languages using only 
the abstraction mechanism; the combinatory calculus of Curry[12] exemplifies 
the use of primitives without abstraction. Curry[12] has demonstrated the 
equivalence of these mechanisms, with minor qualifications, and the choice 
between them for our purposes is largely a matter of c ante riierttf©; we provide 
here syntactic constructs for both. 

Beyond these constraints, the syntactic details of the languages discussed 
here are not important. A LISP-like syntax has been chosen, for the 
development of the models and to provide a definite basis for examples and 
illustrations, although the results and examples %ay be translated to conform 
to other syntactic conventions which are consistent with these constraints. 
Syntactic characteristics of our model languages include: 

1) A finite alphabet including the alphanumeric characters and the special 
characters "(" and ")"; 



2) A countably infinite set of identifiers , eanh a finite string of 
alphanumeric characters of which the first is alphabetic; 

3) A set of numeric constant*, each represented in the language by a finite 
string of digits* 

The elements of the model applicative languages are the applicative 
expressions (A£'s) whose syntax is given by: 




<AE list> 

<lambda expression> 





:= <identifier> | <number> ! <combination> | <lambda 

:» <letter> ! <identifier><di#it> ! <identifier> 

= ( <AE list> ) 

= <AE> ! <AE> <spac«> <AE list> 

= ( LAMBDA (<bvl>) <AE>) 

= <null> i <identifier> <space> <bvl> 

= <digit> ! <digit> <nuaber> 

= A i B i . . . i Z 

= 1 i 2 ! ... ! o 

We assume of these model languages that data is eitfcar numeric or functional, 
that is, that the value computed for any applicative expression must be either 
a natural number or a function. 1 An expression X is atomic if X is an 
identifier or a number; in addition the following syntactic forms have special 
meaning in our model languages: 

1) The syntactic form of a lambda expression is 

(LAMBDACa, a_ ... a ) b) 
i c n 

«„9S£ lt£i s i? n t0 i 8 nore u f o r the present other common data types (floating 
po i n L?V mbers ' arravs » character strings, lists) is Justified by their 

Sa^ ™v L a L?!i™5fri„ s 2w£ hat our r esul £ s concerning processing of numeric 
data may be extended to the processing of these other data as well. 

2.1 -17- 

where LAMBDA is a reserved identifier in the language, the a are 
identifiers on the bound variable list of the lambda expressions, and the 
expression bis the body of the lambda expression. 

2) The syntactic form of the application of the procedure (function) f to 

arguments x. ... x is 

(f x, . . . x ) 
i n 

Here f is presumed to be the representation of a functional datum, and 
the x are representations of arbitrary data which are supplied to the 
function f as arguments . 

There is in each language a small finite set of reserved identifiers used to 
denote primitive functions. Our initial models will include the following 
primitive function identifiers: 

1) The logic values T and F, primitive functions defined such that the value 
of the application 


is the value of the expression a., regardless of whether the value of the 
expression £, is defined. Similarly, the, value of 

(F a b) 
is the value of the expression & whether or not a. has a value. 

2) The function PLUS of 2 arguments, defined such that the value of the 

(PLUS a b) 

is the sum of the values of the expressions a. and St. Tbe value of the 
application of PLUS is undefined if either of the values of a. or b_ is 

3) The function GREATER of 2 arguments, defined such that the value of the 

(GREATER a b) 

-18- 2.1 

is the primitive function T if i has a higher numeric value than the 
expression b_, and F if the value of a_ is less than or equal to the value 
of b. 

We shall often refer to an identifier which is not a primitive function symbol 
as a variable . An occurrence of the variable y_ in the expression X will be 
termed a free occurrence if one of the following applies: 

1) X is identically the variable y; or 

2) X is of the form (A, ... A ) and the occurrence of y is free in one of 


the A ; or 

3) X is of the form (LAMBDA(a ... a.)M), y does not occur in the bound 
variable list (a. ... a ), and the occurrence of y is free in M. 

An occurrence of the variable y which is not free is b^und.. 

2.2: Curried Functions 

The syntactic provision made here for functions of multiple arguments requires 
certain further elaboration. We may reasonably demand, for example, the 
ability to express the function MPLUS defined such that the value of tMPLUS m ) 
is the m-ary function which returns the sum of its m arguments. Such 
functions are, in general, unrepresentable unless some primitive mechanism is 
provided within the language for the abstraction of multiple argument 
functions. We might consider, the abstraction primitive ALPHA, defined such 
that the value (ALPHA F G m) is the m-ary lambda expression 

(LAMBDA(X 1 ...X )(G X m (F X, ... X .))) 
1 m m l ra—i 

where F and G are presumed to represent (m-D-ary And binary functions, 

respectively. We might then define MPLUS so thj*t (MPLUS 2) returns PLUS, and 

(MPLUS n) returns (ALPHA (MPLUS n-1 ) PLUS n) for n>2. 

Such a primitive is, however, unnecessary in most languages. The technique of 
Curried functions may be used to couch multiple-argument functions in terms 

named in honor of H. B. Curry who developed this technique; see [12] 

2 ' 2 -19- 

of unary functions, whence the application of F to arguments A A ...A 
becomes n 

( ... ((F A ) A.) ... A ) 
1 «... n 

and the n-ary lambda expression (LAMBDAU, A.,. . .A^>M* becomes 

(LAMBDA (A 2 ) 

(LAMBDA (A n )M) ... )) 

The convention of Curried factions simplifies the presentation of proofs and 
interpreters, as only single argument Amotions need fee ^natdered; m 
therefore hastily adopt it for our present, purposes. Tfce conventional 
multiple argument syntax is slightly less complicatec| f bovver, and tends to 
greater clarity than the use of Curried function*; wft ^onaa^uently allow 
ourselves the informality of switching freely betwa«V *M two conventions at 
our convenience. We may then consider instances of t^ multiple argument 
syntax as an abbreviation for the corresponding Curried ^rntax, which we take 

as basic. 

An exception must be made in the first model language presented, however, as 
the FUNARG problem does not interact gracefully with Curried functions; hence 
in this case the assumption of single argument functions is not made. 

2.3: The FUNARG Problem 

We are now in a position to give an example of a functional ly incomplete 
language, which we call S. S is an abstraction of the applicative subset of 
LISP and similar stack-oriented languages; it servea to introduce the notion 
of env4ronm . ent , and demonstrates that certain minimal structural constraints 
on environment handling mechanisms are necessary for t*e= expressibility of a 
particular class of functions. 

-20- 2.3.1 

2.3.1: The S model 

An environment is a linear sequence of ordered pairs (or bindings ) (x,v), 
where x is an identifier and v is a value. Environments are thus a mechanism 
for the use of identifiers as variables, serving to record the values 
associated with each variable. We represent the environment which binds the 
variable X 1 to the value V , X to V , and so on, as 

((x 1 ,v 1 )(x 2 ,v 2 ) ... ) 

The environment structure of the interpreter for S may be viewed as a stack, 
bindings being pushed onto the environment from the left at the start of the 
application of a lambda expression, and subsequently being popped from the 
environment at the completion of that application. The S interpreter finds 
the current value for a variable X by looking, in turn, at each binding 
starting with the leftmost; when a binding whose first element is X is 
encountered, the associated value (the second element of the binding) is taken 
as the value of X. We may describe this operation by defining a primitive 
function Iflfitaifi. of two arguments, corresponding respectively to the identifier 
to be evaluated and the environment in which its value is to be found: 

lookup[x;((X 1 ,V 1 )(X 2 ,V 2 )...(X n ,V n ))]= 
if xaX then V ; 
else lookup[x;((X 2 ,V 2 )...(X n ,V n ))] 

We now describe the interpreter for S as a function defined recursively as 

S[x;e] = 

if x is a number, then x; 

if x is a member of {T,F, GREATER, PLUS} then x; 

if x is an identifier then lookup [x,e]; 

if x is a lambda expression then x; 

if x is of the form (T y z) then S[y;e]; 

if x is of the form (F y z) then S[z;e]; 

if x is of the form (GREATER y z) then: 

if S[y;e]>S[z;e] then T; 

else F; 

2.3.1 -21- 

if x is of the form (PLUS y z) then S[y;e]+S[z;e] ; 

if x is of the form ( (LAMBDA(s, . ..s ) b) y,...y J where the 

in in 

s are identifiers, then 

S[b;(s 1 ,S[y 1 ;e])...(s n ,S[y ;e])e]; 

if x is of the form (y z. z_ ... z) where y is not a lambda 

i z n 

expression, then S[(S[y;e] z 1 ... z n );e]; 
else undefined 

Thus S[x;e] computes the value of the expression £ in the environment e_. 
S[x;0] (where is the empty envi ronmetifc$ computes the value of it on an S 
evaluator in its initial "bare" state; we may refer to this simpley as the JS 
xalus. o£ £. 

2.3.2: Arithmetic Completeness of S 

We refer to a language as arithmetically complete if every computable first 
order 1 function is representable as a procedure of that language, ire show 
that S is arithmetically complete by showing that for every first order* 
partial recursive (hence computable) function there is a corresponding 
function in S. The constructions of this section are adaptations 'or those 
appear*** in DertouK>a£3] and are included >.fc«jBt«irfcpi$& far aalce of 
illustration; while each subsequent medal language 4a; vplso arithmetically 
complete, similar constructions apply in eaoh case and will not be repeated. 

As a preliminary step, we consider the S function given by: 

(LAr«DA(X ¥) 



(PLUS 1 (»-* <MJ« 1 Y)H 
0)) )) 

which computes the "recursive difference" function 

1 Following the terminology of. logic, m ; &pPi*$*?M^™ * e ££?i?ri ?ft y 
numbers in its range and domain, and /^bi^M^jOpdar j pay contain (in 
addition to numbers) functions of order less than J. 

_22- 2.3.2 

D[x;y] = if x>y then x-y else 0; 
by the algorithm 

D[x;y] = if x>y then 1+Dtx;y+1]; 
else 0; 

Note that the extra two layers of LAMBDA bi*d*n« aerve only to bind the free 
occurrence of the identifier D within its own deCAnltiPP, and thus to make the 
recursive function operate properly on S. 

We may define the pr ed ecessor function 

P[x] = if x<1 then else x-1 ; 

in S by the expression: 


where D is the recursive difference function defined above. 

Now we shall demonstrate that every partial recursive function of first order 
is representable as a, function in S. In the following, lower case letters 
represent partial recursive functions while upper case letters denote their 
corresponding S functions: 

1) For every pair of «a««l»al numbers n and m, the m-argument oflaatftQt 
function of va fiie mi* expp •••id in &'*8^ 

(LAMBDA(X. ... X ) n) 
■ m 

2) For every pair of numbers n and m, the m-ary pro lection function which 
returns the value of its nth argument is expressed 4* S by: 

(LAMBDA(X r ...|y. X„> 

3) The successor function i» expressed i^S by: 

(LAMBDA (X) (PLUS 1 X) ) 

1 This is one of several "tricks" which may be used to perform recursion on S. 
The necessity of auch~ tricks, atema fri«JtM^S«^^fiyj|^^e|uacy of^S: the 

jf sf ilsJSf 8S^ oP^|- il^fe itl^^S&^^iyS^*^^ tiS^fo i *P*" a-generai discussion 

2 « 3 ' 2 -23- 

«> (fiSUSaUlfia) For every choice of numbers n and m, m - ary partial 

recursive functions a o a ~> 

"ons gl ... g n> and n _ ary function f> fche m _ a functior 

defined by 

h[x ;x ;...;x ] = f[ a [x * 1 - r n 

12 m 1L8 i LX r*' x m J » ... ,g n [x r ..x m ]] 

is expressed in S as 

(LAMBDAU. ... X )(F 

1 ID 

(G, X 1 ... X m ) 

••• (G n X 1 ••• V » 

where F, G, ... G n are the S expressions corresponding to f and g « 
respectively. 6 r'- 8 n' 

5) (ttlUlla rsfiuxslaa) If the n-ary partial recursive function g and the 
(n*2)-ary primitive recursive function f are expressible in S as G and F 
respectively, then the (n+1 )-ary function h defined by: 

h[x 1 ,...x n ,0] = g[x r ...x n ] 

h[X 1 V^ * ««, X n .y.hCx 1f ...,x n ,y]] 

may be expressed in S by 

(LAMBDA (X 1 ... X n Y) 

((UMBDACX^... X n Y H)(H Xl ... X n Y)) Xl ... X n Y 
(LAMBDA (X 1 ... X n Y) ( (GREATER Y 0) 

(F X 1 ... x n (P Y) (MX, ... X R (P Y))) 
(G X 1 ... X n ) )) )) 

where P is the representation of the predecessor function given earlier. 

6) (iSlizCScjiEslaa) If the (n+1)-ary io^ recursive function h is expressible 
in S by H, then the partial recursive function g defined by 

g[x 1 ;...;x n ] = the Igaat y for which 
htx 1 ;...x n ;y] = 

is represented in S by 

_24- 2 .3. 2 

(LAMBDA (X, ... X ) 

i ■■ n 

( (LAMBDA (R)(R 0)) 

(LAMBDA (Y) ((GREATER (H X 1 ...X Y) 0) 
(R (PLUS 1 Y)) 
Y)) )) 

Finally, we note that the class of recursive functions is by definition 
exactly that class of functions obtainable through finitely many applications 
of the above six rules; hence the S representations given in the rules 
constitute a technique for constructing an S expression which represents any 
function which can be shown to be partial recursive. 

2.3.3: Functional Incompleteness of S 

Recall that the functional completeness of a language L requires that every 
computable function defined on the semantic domain of L be expressible in L. 
Since the natural numbers and (by the preceding section) first order functions 
are included in the semantic domain of S, every second order function is 
definable on the domain of S. The functional incompleteness of S may then be 
demonstrated by showing that a simple second order function is not expressible 
as an S function. We begin by observing that a^e,*igher order functions aj^. 
expressible in S, e.g. the function g, (the "twice" Function} given by 

g[f;x] = f[f[x]J 

is expressible in S as 

(LAMBDA(F X)(F (F X))) 

hence it cannot be argued that ojUy. first order functions are expressible in 
S. The weakness in S which we will demonstrate Involves the inexpressibility 
of certain second order functions, notably f unctions which contain free 
variables and which appear as arguments or values (i.e., bodies) of lambda 
expressions: the so called FUHARG problem, 1 

earlv e SLril^2 e Sfth f i^ FUHARG problem (as well as its name) arose from 
Dertculosf!}]? discussion see weizenbaum[23], Moses[10] or 

2.3.3 _ 25 . 

Consider the unary function f, whose domain contains only integers and whose 
range contains only first order functions, defined by 

f[x] a that function g defined by 
g[y] = x+y 

The function f is computable; it may in fact be expressed in the lambda 
calculus by 


To show that £ is flat expressible in the language of S, the following 
definition is useful: r 

Defn 2.1: We say that the expression a. appears as a subexpression of the 
expression £. if any of the Fol*0wii$ n a1% 'tru*: 

1) The expressions a. and tare identical; 

2) b_ is of the form 

where a. appears as a subexpression of one or more of the b.; 

3) b. is of the form 

(LAMBDAiX, .,.X JB) 
where a. appears as a subexpression of B. 

We say informally that b_ fioj&aina A if A appears as a subexpression of £. 
The basis of the inexpreasibilUy of X in § is eat^^^i* 4^ the proof of 

Lemma 2.2: Let A be any applicative expression and lejt B be a lambda 
expression appearing neither as a subexpression, of A nor in the 
environment e.. Then B does not appear as ^ subexpression of SlA;e]. 

PX2a£ is by induction on the recursion depth of sr*;ej. 

haaiS. For the following syntactic classes of A, the f computation of S[A;e] 
involves no recursion: 

Case 1: A is a number, a primitive function identifier, or a lambda 

expression. Then S[A;e]=A, and the lemma is trivially satisfied as 

-26- 2.3-3 

B is not a subexpression of A. 

Case 2: A is an identifier other than a primitive function symbol. Then 
S[A;e] is lookup[A;e] which cannot contain B since by assumption the 
environment e does not contain B. 

j-nducUpn ; The remaining cases of the syntax of A follow; for these we 
assume that the Lemma holds for recursive calls to S. 

Case 3: A is an application of GREATER or PLUS; the* the value of S[A;e] 
is a number or logic value and does not contain B. 

Case 4: A is the application of a logic value T or F to arguments A., and 
A 2 « Neither A 1 nor A ? can contain B since A does not contain B; 
hence the inductive hypothesis applies tq #ither of the computations 
StA^e] and S[A 2 ;e] and B cannot appear in SC A; e] which is one of 
these values. 

Case 5: A is the application of a lambda expression (LAMBDA ( X, . ..X )M) to 

I n 
the arguments A r ..A n . By the inductive hypothesis, B does not 

appear in any of the values StA^e]. ..SfA n ;e], hence the new 

environment e'=(X 1 ,S[A 1 ;e]). . .(X n ,S[A B ;e] )e does not contain B. As 

a subexpression of A, M cannot contain B; thus the inductive 

hypothesis applies to the value S[M;e'] returned as the value of 


Case 6: A is the application of Y to the arguments A,... A , where Y is 

I n* 
neither a lambda expression nor a primitive function symbol. Y is a 

subexpression of A and by assumption does not contain B as a 

subexpression. Then the inductive hypothesis applies to the 

computation of S[Y;e]=Y', and Y* does not contain B; a second 

application of the inductive hypothesis reveals that B cannot appear 

as a subexpression of S[(Y' A.,. ..A n );eJaS[A;e]. 

These cases are exhaustive, completing the proof. 
We can now characterize a major weakness of the language S by 

2.3.3 -27- 

Thm 2.3: Every function expressible in S whose domain contains only numbers 
may have at most finitely many functions in its range. 

Proof : Functional values in S must be either primitive function identifiers 
or lambda expressions. As there are finitely many primitive functions, 
we need only show that each function of numbers in S has finitely many 
lambda expressions in its range. Implicit in this argument is the fact 
that the number of functions expressed by a Set of lambda expressions is 
no greater than the number of lambda expressions in the set. Each lambda 
expression which contains no non trivial occurrences of free variables 
represents (though not necessarily uniquely) a single function; lambda 
expressions with nontri vial occurrences of free variables (i.e., which 
compute different functions in differing contexts) do not correspond 
semantic ally to functions. 

By lemma 2.2, a function of integers can have lambda expressions in its 
range only if they appear as subexpressions of .the function, since for 
any integer n. and expression £ the expression (£. n.) can contain the 
lambda expression g. as a subexpression only if a; is a subexpression of £. 
As the function must be represented by a finite expression in the 
language S, it may contain only finitely many lambda expressions as 
subexpressions and hence has finitely many lambda expressions in its 

Clearly, the function £. defined at the beginning of this section is a function 
of integers having infinitely many functions in it»«*aage; we conclude that f_ 
is not expressible in S. The problem may be characterised as inadequate 
handling by S of lambda expressions containing free variables. It is apparent 
that free variables are evaluated in the environment in which a function is 
applied, rather than the environment in which it is evaluated. Thus lambda 
expressions with free variables have the property that the computation which 
they perform depends on values in the environment fef their caller; this 
dependency constitutes an implicit input and justifies our exclusion of such 
lambda expressions from the class of functions. Yet proper S functions may 
include such lambda expressions as subexpressions ; witness the S function 

-28- 2.3.3 


>n:ch contains no free variables and hence no implicit inputs. The variable 
a., however, appears free in the lambda expression in its body; this innermost 
j.ambda expression is not a function. The question of the contribution of free 
variables to the functional richness of S naturally arises at this point: Are 
onere functions Which are expressible in S only through the use of free 
variables? Our suspicions lead to the conjecture that every function £ 
-vpressible in S may be represented by an expression F in which no lambda 
expression appearing as a subexpression contains free occurrences of 
variables. This conjecture does not completely deny the usefulness of free 
variables on the S machine. Indeed, lambda exppe*sion« with free variables 

are moderately well behaved when passed downward , i.e., as arguments to 
functions; under these circumstances, the principal danger is due to possible 

conflicts with variables bound by the functions to Which the lambda 

expressions are passed. They may, however, be considered to be "limited 
"unctions" with the qualification that they be applied within the scope of the 
ree variables in their original environment and that they may not be passed 

to functions whose bound variable list includes any of the free variables. 

V..ch qualifications seriously impair the semantic clarity of the language 

imposing them. 

2.4: Evaluation Order 

">.e functional incompleteness of S was shown to he related to the specific way 
:.n which S associates values with, variables in an interpreted program: i.e., 
he environment structure of S* The remaining s*e*l©ns &t this chapter 
resent model interpreters wit* alternative ernrironmem Structures, and which 
-;olve the specific problem demonstrated In Sj- however, they demonstrate 
similar inadequacies in the organisation of control structures r i.e. the data 

structure specifying whioh computations are to be performed and their relative 


Tne notion of control structure has never, to the author s knowledge, been 
fcequately formalized, informally it is the bookkeeping mechanism necessary 
:o resolve algorithms into sequences of operations — e.g., the use of a stack 
o record the return points of calls to a recursive subroutine. 

The first model to be presented is T, similar to S except that its environment 
is structurally a tree rather than a Stack. It is argued that T and S share a 
deficiency which stems from their evaluation order , in particular, from their 
uniform evaluation of arguments regardless of blether the resulting values are 
essential to the computation. T is thus fundtionally incomplete due to 
evaluation order. 

The N model, discussed in section 2.5, is closely related to the normal order 
evaluation of the lambda calculus. It is superior to T in that every 
expression having a T value has an equivalent R value, while certain 
expressions have N values but not T values. » 

2.4.1: The T Model 

The traditional solution of the environment problem of S involves a new 
"internal" representation of a function, oiaai&l' 1 !.' closure. A closure 
includes, in addition to the information in a lambda expression, a 
specification of the environment Jtp which lta f l^ea^ Yariablea e are £o be 
evaluated. As the closure mechanism may^jsequirs the retention of environment 
branches corresponding to fuQOtvign^l app^oj^i,^ /**qm t ,,whicb -control haa^heen 
returned, the envirojwent becomes m i£S& either than f ,^he. M«jm»* &&&.<* S; 
hence we call our new language T. The di^i|anee b»tw,e«n T and S is that in 
T, the lambda expression 

(LAMBDA (a,... a.) b) 

is no longer self evaluating. Its valua, lnenyl^nment a., is 

(FUNAHG(s 1 ...s ) b e) 
i n 

which is the representation of a closure in T. We define T as follows: 
T[x;e] = 

i^ xis^ a number,, then x; 

if x is a member of 4T,*,j3§«Tj^fcysi then x; 

if * is *f» identifier t*en lookup* xjei » 

1 We say an expression X is self evaluating if the value of X is X. 

-30- 2.4.1 

if x is of the form (T y z) then T[y;e]; 

if x is of the form (F y z) then T[z;e]; 

if x is of the form (GR EAT St y z) then: 

if T[y;e]>T[zje] then T; 

else F; 

if x is of the form (PLUS y z) then T[y;e)+T[z;e]; 

if x is of the form 

(LAMK)A(s 1 ...s„) b) then 
i n 

(FUNARG( Sl ...s J b e); 
if x is of the form 

((FUNAHG(s 1 ...s n ) be^ y r ..y n ) then 

T[b;(s 1t Y[yi;e]) ... (s^Tty^eD+e^ ; 
if x is of the form (y z^ z ... z ) where y is not a 

FUNARG closure, then 

Tt(T[y;e3 z t ... z n >;e]; 
else undefined; 

We note that a lambda expression is not applied directly; it is first 
converted to a closure (by its evaluation), and then applied by the evaluation 
of its body in an environment formed by appending the bindings of its bound 
variable list to the closure environment. Thus the free variables of a lambda 
expression are evaluated in the environment in which the lambda expression is 
evaluated. The reader may verify that the function represented in the lambda 
calculus by 


which the preceding section showed to be inexpressible in S, is expressible in 
T (indeed, by the same lambda expression). 

2.4.2: Functional Incompleteness of T 

Except for the special cases involving the application of 1 the primitives T and 
F, the T evaluator uniformly evaluates the expressions supplied to an operator 
as arguments before the operator is applied. This order 1 ©f evaluation, which 
has been termed applicative order , has the virtue that each subexpression of 

2.U.2 -31- 

an AE is evaluated at moat once, whereas in the normal order evaluation of the 
lambda calculus an argument to a function may be evaluated many times. The 
disadvantage of applicative order evaluation is that r arguments may be 
evaluated (once) even though their value is irrelevant to the computation; 
this is not merely a matter of occasional inefficiency, since the irrelevant 
argument may not be defined whereby the entire computation diverges. Consider 
the case of the trinary pro lection function 

P 31 [x;y;z]=x 

which returns its first argument regardless of whether its remaining arguments 
have defined values. The applicative-order counterpart of P is represented 
in T by the expression: 

f 31 =(LAMBDA(X Y Z> X) 

This expression does not return a value under ^-evaluation unless all three 
arguments have defined values. 

Our decision to distinguish between P_^ and f_. in effect recognizes the 
undefined, element. », as a member of the functional domains of our applicative 
languages. Intuitively, • represents the "value" of those computations which 
do not terminate, and whose expressibility in each language L is guaranteed by 
the Turing universality of L. 

We now show that P . is not expressible in T; 

Thm 2.4: For every AE £, the T value of the expression 

(I 3 • •) [2.5] 

(where * denotes any expression whose T value is undefined) is undefined. 

Proof: We consider exhaustively the possible I values of the operator £: 
If £ is a number or a primitive operator, then the value of [2.5] is 
undefined due to an error in functional ity, i.e. the application of a 
primitive to arguments for which it is not defined, may assume that f is 
either a combination or a lambda expression, in which cases the value of 
the combination is the value of the application of the T value of f to 
the specified arguments. If the value of £ is a number or a primitive, 

_32- 2.4.2 

[2.5] is again undefined due to an error in functionality. Hence the 
value of f_ must be a closure. The computation of the application of a 
closure involves binding the values of eaern argument onto the 
environment, hence the evaluation of [2.5] entails evaluation of each 
argument. Since not every argument has a defined T value, the value of 
[2.5] is undefined. 

Since clearly the projection P . has the property of £ in Theorem 2.4, T must 
te functionally incomplete if we are to consider P a function. 


2.5: The N model 

This section introduces an applicative language whose interpretation involves 
normal order evaluation. The superiority of N over T derives from this 
revised evaluation order of N, which permits an expression t° be evaluated 
even though subexpressions of it may be undefined. A theorem of Church and 
Rosser establishes that if an AE, A, has a value under iaSL evaluation order, 
then it has that value under normal order evaluation; thus in terms of 
evaluation order, M is optimal. 

The simplest implementations of normal order evaluation involve the 
substitution of argument text in the bodies of lambda expressions, rather than 
the binding of argument values in environments. While the explication (and 
implementation) of such substitution algorithms is relatively straightforward, 
evaluation by simple substitution is often inefficient since 

1) It involves making many copies of program text during execution, and 

2) It often involves multiple evaluations of the same subexpression. 

for reasons of efficiency, substitution evaluators are thus primarily of 
theoretical interest. 

More efficient implementations of normal order evaluation retain the 
environment structure of the T model, and introduce additional mechanism to 
indicate which bound expressions have or have not been evaluated. Since the 
environment implementations of normal order evaluation involve considerable 

2.5 -33- 

bookkeeping machinery and are hence conceptually much more complex than the 
substitution algorithms, they will not be pursued. 

2.5.1: Axioms for the Lambda Calculus 

The primordial applicative language is the lambda calculus, which has been the 
subject of much investigation since its conception by Alonzo Church in the 
1930s. The semantic basis of the lambda calculus is a set of axioms which 
define an equivalence relation, =, on expressions of the language. Each axiom 
may be interpreted as a conversion rule for reduction rule ) in the sense that 
it provides a means for converting (or reducing) an AE to an equivalent (uqder 
= ) AE having a different form. The presentation of the axioms in this chapter 
is somewhat informal, serving primarily as motivation for the N interpreter; 
the interested reader is referred to Curry[12] and Hindley[21] for further 
detail. Related issues are also covered in greater depth in later chapters of 
this report. 

The axioms of the lambda calculus are of 4 types, designated alpha 
(equivalence under renaming), beJA (function application), delta (primitive 
function definition), and, in some formulations, ejfcfi. The delta and eta 
axioms are not used in all formulations. The eta axiom seems to serve no 
important function in the evaluation of expressions and will be presented here 
only in passing. The delta axioms may be avoided by well known coding 
techniques which involve the representation of nonfunctional data, e.g. 
natural numbers, as lambda expressions. 

The formulation which will be primarily referred to in subsequent chapters 
comprises the alpha, beta, and delta axioms, and is often termed the 
beta-dej.ta- cal cuius in the literature. Unless otherwise qualified, generic 
references to "the lambda calculus" in this report, denote the beta-delta 

The equivalence relation s of inter convert ability is generated by a relation 

Many such codings are possible: a popular choice represents by the 
expression (LAMBDA (X) (LAMBDA (Y)Y) ) and the number n+1 by 

(LAMBDA (X) (LAMBDA (Y)((N X)(X Y)))) where N is the representation of the number 
n. For development of such a coding, see Church[1]. 

-3M- 2.5.1 

-> of reducibilitv : hence X->Y implies X=Y which, in turn, implies Y=X. 
Reducibility is in general antisymmetric, however; thus -> provides an 
ordering of equivalent expressions which has important ramifications in the 
lambda calculus. The relation -> is defined to be a monotone relation 
meaning that it has the following properties: 

Reflexivity: For every X, X->X; 
Transitivity: If X->Y and Y->Z, then X->Z; 

Monotonicity: If X->Y and B is the result of substituting, in an expression 
A, X for an occurrence of Y, then B->A. 

The relation = is in addition an equivalence relation; hence X*Y implies Y=X. 

Central to the axioms is the substitution rule . S, of fundamental importance 
to the lambda calculus as well as the theories of the following chapters of 
this report. S is formulated as a three argument function, such that the 
meaning of S[X;Y;Z] is roughly "the result of substituting the expression X 
for free occurrences of the variable Y in the expression Z. The definition of 
S is further complicated, however, by the requirement that the operation 
S[X;Y;Z] not introduce conflicts between free variables in the expression X 
and bindings of X within Z. There is a long history iof incorrect algoritms 
for S; the definition given here is due to Curry: 

Defn 2.6: For expressions X and Z, and variable Y, the expression S[X;Y;Z] is 
defined as follows: 

1) If Z^Y, then X; 

2) If Z is a primitive, number, or identifier other than Y, then Z; 

3) If Z is of the form (Z 1 Z £ ) then (SCXtfjZ,} S[X;Y*;Z g ]); 

4) If Z is of the form (LAMBDA(A)M) where Y=A, then Z; 

5) If Z is of the form (LAMfiDA(A)M) where ¥ is different from A, then 
(UMBDA(B)S[X;Y;S[B;A;M1T). where the variable B is chosen as follows: 
i) If Y does not occur free in M or if A is not free in X, then B=A; 
ii) Else B is any variable which ooeurs free neither in M nor in X. 


Terminology after Curry[12] 

2.5.1 -35- 

We now procede to the statement of the axioms: 

Axiom alpha : If E is a lambda expression of the form (LAMBDA(X)M) and the 
variable Y does not occur free in K, thftfi £^jLAl|HM<X>S{Y;X;M]). 

We say that expressions A and B are co rurruept if A can be converted to B by 
alpha conversion alone. No^te that if , X->Y by alpha conversion then Y->X by 
alpha conversion; hence X=Y. Congruence is thus symmetric and transitive, 
and under most circumstances congruent expressions may be treated as 
identical* We say that expression X Is in normal form if the only reduction 
which can be performed on X is alpha conversion. 

Axiom beta : If E is an, expression of,,the fora ( £UH8pA(X)M) A) then 
E->S[A;X;M], ..,,. 

Axiom fila: If E is an expression of the form (LAMBDA(X)(M XJ) where X does not 
appear free in M and M is a lambda expression, then E->H. 

Axiom delta : If E is an expression of the form (F A, A '... A ) where F is a 

i e. n 

primitive function symbol and each Ai is in normal form and contains no 

free variables, then E->f[A,;. ..;A J where t Is the operation denoted by 

1 n 


The following two theorems are of fundamental importance in the lambda 

calculus. The first is dbe, in its Initial primitive form, to Church and 

Rosser and is referred to in the literature as the Church-Rosser Theorem: 

Thm 2.7: Let X and Y be expressions such that XxY. Then there exists an 
expreslon, 2-, such that X->Z and Y->Z. 

proof may be found in Curry[12] or HindleyC21] and elsewhere. 

The Church-Rosser Theorem shows that the lambda calculus is consistent in the 
sense that the relation = is nontrivial; in particular, X=Y is not true for 
incongruent expressions X and Y in normal form. We can thus prove that 
expressions X and Y are not interconvertible by finding normal forms X' and 

This definition is recast more formally in the terminology of Chapter 4. 

-36- 2.5.1 

Y , where X->X' and Y->Y', which are incongruent. 

Unfortunately, not every expression X is convertable to an expression X' in 
normal form. For example, the important expression 

Y= (LAMBDA (F)( (LAMBDA (H)(F (H H) }>(LAMBDA(H) (F (H H))))) 

which is the "paradoxical combinator" of Curry, has no normal form. Further 
discussion in this area follows in Chapters 1 and 5, along with related 
technical developments. 

A second important theorem, due to Corrado Boehm, has, been proved only for 
systems which prohibit delta conversions: 

Thm 2.8: Let X and Y be incongruent expressions in normal form, and let C and 
D be arbitrary expressions. Then there exists and expression Z such that 
C=(Z X) and D?(Z Y). 

Proof originally appeared in Boehm[20], in Italian; a proof in English 
appears in Curry[27]. 

Boehm's Theorem guarantees that incongruent normal forms, in the beta- eta 
calculus are semantically distinct; in particular, the axiomatic assertion 
that any two incongruent normal forms are interconvertible results in an 
inconsistency. The extension of Boehm's Theorem to systems, which include 
delta conversions requires that the constants added to the pure lambda 
calculus also be semantically distinct. We might, for example, formulate a 
calculus including the numeric constants without providing any means for 
distinguishing between them: we could provide the primitive PLUS but not 
GREATER. While this formulation is valid in terms of the lambda calculus, 
Boehm's Theorem is clearly inapplicable since there is no expression Z which 
distinguishes, say, between the normal forms 2 and 3. 


deltI'conve l rsio , S" lati0n lncludin « axioms al P na . bet *. and eta, but excluding 

2.5.2 -37- 

2.5.2: Normal order: Substitution 

Each of the lambda calculus axioms provides a means by which an applicative 
expression E may be reduced to an equivalent expression E'. While the axioms 
themselves place certain restrictions on the order in which such reductions 
may be performed, 1 the evaluator of an applicative expression has a great deal 
of freedom to choose the order in which to evaluate subexpressions. 
Normal order evaluation specifies that at each evaluation stage, the leftmost 
reducible subexpression is to be converted. The N Evaluator 

We define the N value of an AE x as follows: 

N[x] = 

if x is a number, then x; 

if x is a member of {PLUS, GREATER} then x; 

if x is a lambda expression, then x; 

if x is of the form (PLUS a b) where N[a] and N[b] are 

both defined and numeric, then N[a]4N[bJ; 
if x is of the form (GREATER a b ) where N[a] and N[b] 

are both defined and numeric, then if N[a]>N[b_] then 

(LAMBDA (X Y)X) else (LAMBDA(X Y)Y) ; 
if x is of the form ( (LAMBDA (a) b)c_) where a is an 

identifier and band c are AE's, then N[b'] where b' 

is the result of substituting c. for each free 

occurrence of a in Jb; 
if x is of the form (a b) where a and b are AE's and a. 

is not a lambda expression, then N[(N[a] b)]; 
else undefined; 

Note that we have eliminated the primitives T and F, which are entirely 
equivalent in N to the lambda expressions which replace them as values of 

OY ^f ^ e x P ress i on .E containing applications of lambda expressions, for 
example, is beta-reducible. Applications ofaxiom alpha, ie the renaming of 
variables, may be required before axiom beta is applicable! renami ng °r 

-38- Axiomatic Consistency of N 

We show in this section that N evaluation is consistent with the semantics of 

the lambda calculus by demonstrating that N preserves the equivalence relation 

Thm 2.9: Let E be any AE such that H[E] is defined. Then E->N[E] where -> is 
the reducibility relation defined by the lambda calculus axioms. 

proof : by induction on the level of recursion in the computation of N[EJ. 
basis : if E is a number, a primitive, or a lambda expression then N[E].=E. 
induction : we assume that the Theorem holds for recursive calls to N. 
Then the Theorem holds for the remaining syntactic cases of E by the 
monotonicity of ->. 

We note in passing that H[E] is not necessarily a normal form. Lambda 
expressions, in particular, are not reduced by H r since otherwise the 
evaluation of certain meaningful expressions (e,g. the paradoxical combinator 
Y) would not terminate. 

2.6: Functional Domain of N 

In this section it is shown that the entire domain of N constitutes a 
functional domain satisfying the intuitive criteria of [1.1]. We interpret 
the semantic equivalence relation, ", on the domain of N as follows: 

For X,Y in D N , X~Y if and only if [2.10] 

for every Z in D and number n f 
(Z X)=n <=> (Z Y)*n 

where D is the domain of N* We now justify this interpretation of " on N 



Thm 2.11: The domain of H is a functional domain, obeying the criteria of 
[1.1], under the above interpretation of ". 

proof : The equivalence relation ~ defined in [2.10] must be shown to obey 

2.6 _39- 

the three clauses of [1.1] over the domain D„ of N. We treat the clauses 



1) For numeric constants X and Y, we must show that X"Y <=> X=Y. 
<=: direct, by the equivalence of identical expressions. 
=>: Assume X~Y. Then by beta-reduction, 

((LAMBDA(a)a) X)=X 

((LAMBDA(a)a) Y)=Y 

and thus, by [2.10], X=Y since they are numeric. By [2.7] there exists a 
Z such that X and Y are each reducible to Z; since X and Y are not 
reducible, Y, Y, and Z must be identical. 

3) To show: X~Y <=> for all Z in D , 

(Z X)~(Z Y) or neither defined. 

=>: Assume false. Then for some X~Y there exists a Z such that 

(z 1 X)T(Z 1 Y) 

where | is the negative of ~. This implies, by [2.10], that there exists 

a Z_ such that 

(Z 2 (Z 1 X))=n 

for some numeric constant n but not 

(Z 2 (Z 1 X))=n 

(we are assuming here one of two completely symmetric cases with no loss 
of generality - the other case follows by interchanging the symbols X and 
Y). Defining Z by the lambda expression 

we note that 

hence by [2.10] X|Y. 

Z 3 =.( LAMBDA (a )(Z 2 (Z, a))) 

(Z X)=n but (Z Y)*n 

-40- 2.6 

<=: Assume that for all Z in D , (Z X)~(Z Y). Then (Z X)=n (for numeric 
constant n) if and only if (Z Y)=n by the argument of part (1). Hence by 
[2.10] X~Y. 

2) It must be shown that X~Y if and only if for all Z in D N , (X Z)~(Y Z). 
From part (2) of this proof, X~Y <=> for all Z: 

((LAMBDA(a)U Z)) X)~( (LAMBDA(a) (a Z)) Y) 

hence, by beta-reduction, 

(X Z)~(Y Z) 

The significance of Theorem 2.11 is that every element of the domain of N 
corresponds to some element of the abstract semantic domain: every element of 
D. T is intuitively functional. Thus N (and the lambda calculus on which it is 


based) is a language of "pure" functions. We shall find in the next chapter 
that this pleasant property costs us something, however, in terms of 
ex pr es s ive powe r . 

2.7: Summary 

The material in this chapter is largely introductory. The three interpreters 
presented are abstracted from conventional implementations, and their scrutiny 
serves to relate common implementation issues to the expressibility of 
functions. The major findings were: 

1) Each language is arithmetically complete, in the sense that every 
computable function defined on the natural numbers is expressible. 

2) The FUNARG problem leads to the inexpressibility in S of functions whose 
domain contains integers and whose range contains infinitely many 

3) Applicative order evaluation renders inexpressible in T every function 
whose domain includes *, the undefined computation. An example of such a 
function is the constant function (LAMBDA(X)3) of one argument. 

2.7 -41- 

4) The interpreter N, based on the normal order evaluation of expressions by 
substitution, suffers from neither of these deficiencies. We can 
construct a functional domain F such that every expression X in the 
domain of the language N corresponds to an element of F; thus N is a 
"pure" language in the sense that every expression corresponds to a 
function or a number. This is not true, for example, in S, where lambda 
expressions containing free variables can compute different functions in 
varying contexts. 

We are left with N, an interpreter whose behavior is intended to model the 
lambda calculus; the remainder of this report, roughly speaking, deals with a 
particular weakness common to N and the lambda calculus. 

This empty page was substituted for a 
blank page in the original document. 

3 -4 3- 

Chapter 3: 
Motivation for a Multi-valued Semantics 

Central to this chapter is the argument that the N model, and hence the lambda 
calculus, is functionally incomplete because of the inexpressibility in N of a 
class of computable functions on N's domain. The inadequacies of N leading to 
this weakness are explored, and two new model languages are presented, each 
curing the problem in a different manner. The first model, which has 
provision for encoding representations of functions as integers, is found to 
be unsatisfactory for both practical and semantic reasons. The alternative 
solution proposed in this chapter involves mechanism for the representation of 
semantic elements with multiple values; this mechanism, called EITHER, is the 
principal focus of the remainder of the Thesis. 

3.1: Necessity of non-functions: WHICHFF 

Consider the family of partial functions, {FF. } for i ranging over N, which 
satisfy the following conditions: for each natural number i., 

FF 1 Ex] = i, i=x [3.1] 

divergent, i^x 

Thus each FF has a single element in its domain: the number i. For any other 
argument the value of FF [x] is undefined. The {FF. } are clearly partial 
functions in the intuitive sense of Defn [1.1], and are computable in each of 
the model languages considered here. Furthermore, they are semantically 
distinct: for no numbers i*j does FF -FF.. There is then nothing intuitively 
objectionable about a function which maps each FF. to its corresponding i. 
Consider such a function WHICHFF which, for each natural number i., has the 
property that: 

WHICHFF[FF. ] = i [3.21 

Intuitively WHICHFF is a function from {FF. } onto N; furthermore it is 
demonstrably computable using "dovetailing" or multiprocessing techniques. 
Note in particular that the following definition of WHICHFF satisfies the 
condition of [3.2] : 

-44- 3.1 

WHICHFF[f] = i such that f[i3=i, C3-33 

if such a number i exists; 
else undefined 

We may view the dovetailed evaluation of WHICHFF£f] as the computation of f[0] 
for one second, the computations of f[0] and f[1] each for two seconds, and 
similarly until any one of the computations f£i] terminates normally; the 
value of this f[i] would then be taken as the value of WHICHFF[f]. However, 
WHICffiT is not expressible in N; this is a result of 

Thm 3.4: Let L be an arithmetically complete applicative language and let D 
be the domain of L. Then no function WHICHFF having the properties of 
£3.33 is functional over D^. 

proof by reduction to the halting problem. Assume that D, contains a 
function WHICHFF having the property given in £3.3]. Then for any 
function f in D, and any number 1, Lt (WHICHFF £)3"i if f_~FF i . How 
consider the union of the functions FF, and FF , given by: 

FF t2 £x] = 1 r L£x]=1; 13.5} 

2, L[x]=2; 
divergent otherwise 

FF 1? is clearly a computable first order function, hence it is 
expressible in L by the arithmetic completeness of L. Now L[ (WHICHFF 
FF J] can have as its value at most one of {1,2}; thus either L[ (WHICHFF 
FF _)]*1 or L[ (WHICHFF FF )}#2. Assume, with no loss of generality, the 
former. Then define the second order function g. as follows: 

g[f] = the function g , where 

g f Ci] = 1, 1=1; 

2, i=2 aM f£0] defined; 

divergent otherwise. For every computable 
first order function f, g. (or equivalently g£f]) is evidently 
computable. Moreover, if f [0] is undefined then g_ is identical to the 
function FF^; otherwise g_ is identical to the function FF We use the 

ability of WHICHFF to distinguish between FF 1 and FF 12 to determine 
whether f[0] is defined, by means of the function & given by 

3-1 -45- 

h[f] = WHICHFF[g[f]] 

We note finally that for any function f 

f[0] convergent => g[f] - FF 12 => h[f]*1 ; 

f[0] divergent => g[f]~FF => h[f]=1 

Hence h[f]=1 if and only if f[o] is divergent. The divergence of f[0] is 
decidable, as one of the computations h[f] and f[0] must converge; thus 
the function h provides a solution to the "halting problem" for first 
order functions, and is a well known noncomputable function. Since h is 
clearly computable in terms of WHICHFF, we conclude that WHICHFF is not a 
computable function over any domain including the first order functions. 

Since it was shown in the last chapter that every function expressible in N is 
functional over all of the domain of N, it follows that WHICHFF is not 
expressible in N. This inexpressibility relates intuitively to two aspects of 
the implementation of the N interpreter: 

1) The interpreter does not admit multiprocessing. If, in the evaluation of 
expression A, N embarks on the evaluation of a subexpression a of A whose 
N value is not defined, then the N value of A is not defined. 

2) The only mechanism in N by which a function f can recover information 
about its functional argument g. is the application of g.. There is no 
means by which f can discover the algorithm (or program) by which g. 
computes values, even though the internal representation of g. necessarily 
includes this information. Hence if f is to make any use of g., then g. 
must be applied to some argument; By the constraint (1) above, the 
nontermi nation of this application results in the nontermi nation of the 
application of f. 

The correction of either of these deficiencies is straightforward in an 

implementational sense — many extant languages boast provisions for 

multiprocessing and/or access to representations of functions. However, 

neither "correction" is easily record i<>h , ,■,•<- v. *u~ 

' Ict -°nciled with the semantics of an applicative 

language. The second limitation of N seems a natural consequence of our 

-46- 3.1 

distinction between the notions of a function f and any of the algorithms for 
computing £ from its arguments; a language which provides mechanism for 
distinguishing between algorithms for computing a particular function f. would 
certainly have non-functional elements in its domain. The semantic 
ramifications of a cure to the first problem, however, are more subtle and 
will be explored in detail. 

The following sections present two alternative extensions to N, each 
corresponding to a "fix" of one of the above limitations. The function 
WHICHFF is expressible in each. 

3.2: Coding primitives: The C model 

We noted that a limitation of N, justifiable by our intuitive respect for the 
semantics of functions, is that no information can be recovered about an N 
function without the application of that function. In particular, S provides 
no means for recovery of information about the representation of a function as 
an N expression. We have thus avoided the "Turing Machine tar pit" « the 
argument that any language as powerful as a Universal Turing Machine has 
exactly the same set of expressible functions. 

The C model presented here has, in addition to the primitives and structure of 
N, primitives for the translation of the representation of language elements 
to and from a tractable form. Making the fundamental assumption that any 
function defined on a domain F is computable if and only if it is computable 
from the representations of elements of F, we must conclude that a Universal 
Turing Machine (or its equivalent) operating on the representations of 
arguments to the computable function f can compute representations of the 
values of £. This is the substance of our claim of functional completeness of 
the language C. 

The interpreter for C is identical to the interpreter for N except for the 
addition of the primitive operators CODE and WECtfDE. CODE maps 
representations of the domain of C into the natural numbers: 

CODE: D c -> N 

3.2 -47- 

and may be viewed as a Goedelization of the character string representing its 
argument. The claim we make for CODE is that if (CODE X) and (CODE Y) have 
the same (numeric) value then X and Y are semantically equivalent; they are 
in fact represented in an identical manner. We cannot, of course, claim that 
in general X~Y implies (CODE X)=(CODE Y), as there are many representations of 
each semantic element and the semantic equivalence of the representations is 
effectively undecidable. The operator DECODE is the inverse of CODE: given 
the Goedel number of the representation of an element, it returns the element. 
We thus claim that each expression X is semantically equivalent to (DECODE 
(CODE X)). 

Our claim for the functional completeness of C is formalized, to the extent 
possible, in 

Thm 3.6: Let F be a functional domain of C, and let 

g: F -> F 

be a computable function on F. Then g is expressible in C, i.e., there 
is an expression G in the domain of C such that for all x,y in F, g[x]=y 
implies that (G X)~Y. 

proof : Since g is computable then so is h defined by: 

h = (LAMBDA(Y)(CODE (g (DECODE Y)))) 

as it is simply the composition of computable functions. Furthermore, 
since h is a function from N to N, it is expressible in C by the 
arithmetic completeness of C; let H be the representation in C of h. 
Then the function g is expressible in C by: 

G _= (LAMBDA (X) (DECODE (H (CODE X)))) 

It must be recognised that CODE is not functional: it radically disobeys the 
intuitive requirements of Defn 1.1. We note, for example, that CODE might 
return different values for the arguments (LAMBDA(X)X) and (LAMBDA(Y)Y) as 
they have different representations, violating our requirement that 
semantically equivalent arguments produce semantically equivalent results. 

-48- 3.2 

WHICHFF example of the preceding section. The representation of WHICHFF in C 
involves writing an interpreter, operating on the CODEd representations of C 
expressions, which simulates the required "dovetailing" by computing 1 step of 
(g 1), 2 steps of (g 2), 2 steps of (g 1), etc. Presentation of actual code 
for WHICHFF on C would be, at best, a messy task; it is hoped therefore that 
the reader will accept the expressibility of WHICHFF in C on the basis of 
Theorem 3.6 and this informal discussion. 

3.2.1: The Turing -ma chine Tar Pit 

The introduction of the specter of coding requires further reflection. We 
have made the enticing observation that, with the introduction of a simple 
mechanism allowing the representations of functions to be accessible as data, 
every computable function becomes expressible. We have noted corollary 
disadvantages — (i) the semantic confusion resulting from the nonfunctional 
character of (DDE, and (ii) the practical absurdity of having to include the 
code for interpreters in the definitions of certain functions. 

However, the inclusion of coding primitives in an applicative language may be 
objected to on more fundamental grounds than the above. The stated semantic 
goal of an applicative language is the representation of functions. Thus such 
a language provides a set of rules and conventions for associating expressions 
with abstract functions; moreover, the power and consistency of the language 
stem largely from the applicability of these rules and conventions to every 
expression in the language. In the lambda calculus, for example, we are 
assured that expressions which are interconvertible via the alpha and beta 
axioms are equivalent. The cost of this assurance is a corresponding 
constraint on the computations which we might perform: the alpha axiom 
positively prohibits us from writing a function which distinguishes 
(LAMBDA(X)X) from (LAMBDA(Y)Y). We accept this constraint because the 
structure which it imposes is useful to us; we recognize that we cannot be 
assured of a relation and simultaneously be allowed to violate it at will. 

Coding primitives may be viewed as a mechanism for violating the structure 
imposed by an applicative language. None of the lambda calculus axioms, for 
example, are valid in the presence of coding, since "functions" can be written 

3.2.1 -49- 

which distinguish between interconvertable expressions. The rules and 
conventions for representing functions are, in effect, abandoned. The 
programmer is thus freed from the structural constraints of the language, but 
finds himself in a semantic anarchy - while he may write any function he 
Pleases, he may make no assumptions about the structure or representation of 
its arguments. 

3.2.2: Functionality of DECODE 

We may convincingly defend the contention that CODE is not a function by 
demonstrating that it returns semantically distinct integers, say, for the 
equivalent arguments (LAMBDA(X)X) and (LAMBDA(Y)Y). This demonstration does 
not apply, however, to the inverse of CODE; there is nothing inherently 
nonfunctional in the fact that DECODE returns semantically equivalent 
expressions (LAMBDA(X)X) and (LAMBDA(Y)Y) when given semantically distinct 
integers as arguments. It is the purpose of this section to demonstrate that 
functions with the property of DECODE (i.e. mapping a subset of the natural 
numbers onto the entire domain of discourse) are expressible in N and the 
lambda calculus. LAMBDA-free AEs 

It is convenient for certain purposes to use the techniques developed 
primarily by Curry[12] of the calculus of combinatory for the reduction of 
applicative expressions to equivalent expressions whose use of lambda 
expressions is highly restricted. For our purposes we shall consider the 
combinators listed below (along with their respective definitions): 

I =. (LAMBDA (X)X) 


W =. (LAMBDA (X) (LAMBDA (Y)(X Y))) 

S =. (LAMBDA(X) (LAMBDA (Y) (LAMBDA (Z)((X Z)(Y Z)))) 

G 1 =. (LAMBDA (G) (G G) ) 

G 2 = (LAMBDA (G) (LAMBDA (Y)(Y G))) 

G 3 =. (LAMBDA (Y) (LAMBDA (X)((Y X) X))) 



We show in this section that every applicative expression using no lambda 
expressions other than the above combinators; we begin with 

Lemma 3.7: Let R be a LAMBDA free AE in the single argument applicative 

language L, and let R contain occurrences of the variable x. Then R is 
equivalent (by alpha and beta axioms) to a LAMBDA free AE of the form (R' 
x) where R' contains no occurrences of the variable x. 

proof is by structural induction on R. 

basis : R is atomic (in particular, R is not a combination). If r is the 
variable x, then r' is (I x)=x (by axiom beta). If £ is not the variable 
x_, then r. contains no free occurrences of & and r' is ((K r) x) = 
((LAMBDA(X)r) x) = r. 

induction : R is a combination of the form (R. R 2 ). By inductive 
hypothesis, R=((R ' x)(R ' x) ) for some AEs R ' and.R ' not involving the 
variable x; then R'=(((S R 1 ) R g ) x) = ( (LAMBDA (X) (LAMBDA (X) ((R 1 X) (Y 
X))))) = ((R 1 x)(R 2 x)). 

The principal result of this section is the following adaptation from Curry's 
Synthetic Theory of Combinators: 

Thm 3.8: Let A be an AE in a single-argument applicative language L whose 
semantic equivalence obeys axioms alpha and beta. Then A is equivalent 
to a LAMBDA-free expression A* containing only the combinators I, K, W, 
S, G., G_, G,, Gh, and the primitives and constants of L. 

proof : We show that, given any such A which is not LAMBDA-free, we can 
construct an equivalent A' containing fewer LAMBDAS. Let a. be an 
innermost LAMBDA expression occurring as a subexpression of A. We then 
construct A' by replacing a as follows: 

Case 1: a. is of the form (LAMBDA(x)x) for some variable x; we replace a. 
by I (equivalent by axiom alpha). -51- 

Case 2: a is of the form (LAMBDA(x)y) where x and y are different 
variables; we replace a, by (K y). 

Case 3: a is of the form (LAMBDA(x)(b x)) where x is a variable and b is 
an AE: replace a by (W b)=(LAMBDA(Y) (b Y) ) 

Case 4: a is of the form (LAMBDA (x)(c d)): By Lemma 3.7, the body (c d) 
is equivalent to an AE (r' x) where the variable x does not appear in 
r'. Then a=(LAMBDA(x) (r ' x) ) which is reducible according to case 3. 

Since each expression A which is not LAMBDA free is thus equivalent 
to an expression A' containing fewer LAMBDAS, a finite number of such 
reductions will reduce each such A to a LAMBDA free A*. This completes 
the proof. 

It is a relatively simple exercise to show in addition that each of the 
c xnbinators I, W, G^ G 2 , G_, G^ is in turn equivalent to an expression in K 
and S, allowing us to simplify Theorem 3.8 by eliminating all but 2 of the 
combinators. This is unnecessary for our purposes, however, so long as the 
number of combinators required is finite. An important observation to be made 
at this point is that the construction of A* detailed in Theorem 3.8 is 
ef fective ; thus we could program a computer to convert AEs to LAMBDA free 
form.,: An Enumeration of D„ 


In this section it is demonstrated that the domain of every applicative 
language with the power of the N model contains functions which .enumerate the 
domain of that language, ie, each such language L with domain D contains a 



f: N -> D 
such that for every finite expression x. in D there is a number n. which 


satisfies (f n)=x. We procede by Goedelizing the LAMBDA free expressions of 


Let pair be a number pairing function such that, for each i and j in N, the 
value of pair[i,j] is a unique number P ±J , and let left and right be functions 
recovering the components of a pair; ie, for every i and j, left[pair[i, j]]=i 
and right[pair[i,j]]=j. There are many well known such pairing functions; 
since they are all first order computable functions, we may assume that they 
are expressible in each of our model languages. 

Let us now suppose that we label the (finitely »ny> primitives of the 
language L as p,, P 2 , ... P„. Note that we include the combinators K, I, 0,, 
etc in this list so that we can enumerate LAMBDA free expressions only. We 
now specify the coding details: for each LAMBDA free expression x, we define 
the Goedelization &[x] as follows: 

g[x] = 

if x is a number then pair[0;x); 

if x is a primitive p. then pair[1;j]; 

if x is a combination (a b) then pairleUbgEb] ]; 

The function * is computable from t*e representation of x, but we cannot in 
general claim that it is computable from the functional properties of x. The 
function k is, in fact, a satisfactory choice for the CODE function of the C 
■od.1. assuming (as we may) that we are content to deal with LAMBDA free 
expressions of C. If such a function * could be shown to be computable in, 
for example, the N model, we would have a direct a. pxiori demonstration that 
the languages are expressively equivalent. We must, however, be content with 
the expressiblity of a semantic inverse of &: the function ejm defined such 
that, for every LAMBDA-free expression x_, enu[g[x]]=x. This apparent 
asymmetry can be explained by the observation that g. is not a function, in the 
sense of Defn [1.1] which prohibits the mapping of semantically equivalent 
expressions into differing numbers. The fact that ejm. may map different 
numbers into semantically equivalent values is consistent with its 
functionality. We label the expressibility of enu. as 

Thm 3 9: Let L be an extension of N with primitives 11, 12 In 

(including combinators K and S). Then there is a function enu_:N->D L such 
that, for every LAMBDA free expression x in D L , there is a number i such 
that enu[i]"x. -53- 

proof is a straightforward programming job. Such a function for the 
language N would take the form: 




((GREATER (RIGHT N) n-1 ) In 

(RIGHT N) ))))) 

where li is the ith primitive of N, and LEFT and RIGHT are the N 
expressions corresponding to the ^eft^ and r ^ ft fr functions above. 

3.?: E model: Multiprocessing primitives 

An extension to the N interpreter which is somewhat more palatable than the 
use of coding primitives is the addition of mechanism for multiprocessing: the 
quasi-simultaneous evaluation of several expressions. We consider here the E 
model, which is the IN model of Chapter 2, augmented by the primitive operator 
EITHER whose interpretation is as follows: 

For every choice of expressions a. and b_, [3.10] 

E[ (EITHER ii)] « 

if E[aJ is defined but E[bJ is not, then E[gJ ; 

if E[bJ is defined but E[aJ is not, then E[b]; 

if E[aJ and E[b_] are both defined then one of these values; 

else undefined. 

Note that we do not specify which of the arguaents is- returned if both have 
defined values; we may consider that this selection iS made by some 
nondeterministic process over which we have no control. EITHER is evidently 
computable by dovetailing techniques, eg by evaluation of E[aJ and EfbJ each 
for 1 step, then each for 2 steos, and so on mnfcil one evaluation or the other 
returns a value. EITHER is not, however, functional: in the case where a and 

- 5 *- 3.3 

b each have defined values (and their values differ), then the value of 
(EITHER a b) is dependent on the representation of a and band on details of 
scheduling of the dovetailed computation. 

The power of the ej^ex primitive is demonstrated by the expressibility of 
WHICHFF in E as follows: 

WHICHFFffJ = gl [f_; ] 

where g^hjfl] = eitherthjnjjg^hjn+l ] 

Note that for i>j, g^FF^i] is undefined and hence for i<j gl [FF.;i],j. Thus 
for every number j, E[ (WHICHFF FF )]=j. J 

The presentation of the EITHER primitive in this section is informal, based 
largely on its intuitive relation to the implementation mechanism of 
multiprocessing. The formalization of this mechanism is a principal topic of 
the remaining chapters. The remainder of the present chapter explores the 
impact of EITHER on the semantics of an applicative language. 

3.4: The Intuitive Paradox 

The reader has doubtless noticed that fundamental questions raised in the 
first section of this chapter demand a more precise characterization of the 
hitherto vauge notion of functional completeness. Specifically, Theorem 3 4 
shows that WHICHFF is not functional over the entity of *ny_ functional 
domain which includes all first order functions. Thus the basic intuitive 
requirements of [1.1] are inconsistent with the existence of a functional 
domain F which is arithmetically complete and tmludss every computable 
function f :F->F. Two alternatives facing us are the following: 

D We can deny that WHICHFF is a computable function. Indeed, Theorem 3.4 
may be interpreted as a statement that no computable function defined on 
first order functions has the properties of WHieffTF given in [3.2] Our 
intuitive claim that WHICHFF is a computable fMctibn Is based on the 
incomplete specification of its behavior otcr -the entire functional 
domain: [ 3 .2] merely defines it over the restricted domain of {FF }. 



2) We can revise the notion of a functional dqmain F such that, for every 
function £ in F there is a dojaaia o£ specification over whicW the 
behavior of f is defined.^ The., functional criteria of [1.1] are then 
required to apply only when the arguments of -£ are drawn from Us domain 
of specification, S . u- ^ - 

3) We can postulate new elements of Afunctional domain F corresponding to 
the values returned by otherwise nonfunctional procedures. 

We reject the first choice on the grounds that it restricts our consideration 
to those functions expressible in the lambda calculus, giving us no way of 
distinguishing between N.and, the ,i«|ui r tivtlys«pwio^B,.Tfte Second choice is 
rejected after brief consideration, (ip.afgilpwing, wefeioi*) ptrW&ecause of 
the technical, complications it entails ^ but mtimmrtly because it denies the 
semantic validity of the interesting <&W^iml*tX*la*%ymLpr* B sl6ria. The 
third choice seems the most, promising, ftq* t*» pofin* of vt«* ^>f rigorous 
analysis, but requires a_ substant^ tnt«4^v* imtp- aAotm^atrulxiiag must be 
carefully scrutinized, This project i* a#proaflfe*<fcfiii subsequent sections? 

3.5: Multi-valued Semantic Elements 

The domain D N of language N was shown, in Chapter .& fco ha** thw^rofiefty that 
every element x. of D^ corresponds to. ex*^y ; 4ms*U*#i& of a ftinetloiwl : 
domain; thus each expression x_ in D N has, intuitively, exactly of* semantic 
value or meaning. In this chapter it was shown that this graceful property 
of D N is ineogsistea* with the^expressiblity of the function ttHICHFF, a 
demonstrably computable anduintuitively weii behaved function "'over a 
particular subset of D^. our i«plea*htati& otWHlC^Ff' while functional oyer 
this restricted domain S, teehaves^p^oi^y %ften given argUme^ts from D,, which 
are not in S; furthemore, this annCying tfefVct 14 characteristic of every ' 
implementation of WHICHFF in a language Wflciehtty powerful as to be " ^ 
arithmetically complete. The problem^ is, e^dfi* **i HHICHFFois applied to 
the function FF^: either of the values 2 or ; y is coaaistentwlth^he 


It must be recalled that w* hav* postulated a semantic element • 

-56- 3.5 

definition of WHICHFF [3.3], and there is no implementation of WHICHFF which 
consistently returns a single value, eg 2, when applied to every x in D 
semantically equivalent to FF 12 . Thus the evaluation of (WHICHFF FF ) leads 
to, exactly the same underdetermlned result as the evaluation of (EITHER 1 2): 
the E values of each expression might be 1 or 2, depending on circumstances 
which are irrelevent to the semantics of each expression,, 

3.5.1: Domains of Specification 

One means of avoiding such apparently hondeterministic computations is to 
exclude them from our semantic model, ie, to deny that (EITHER 1 2) has any 
semantic value. Under this reafrridt ion, we must careMly exclude from our 
consideration any repression having multiple E values, either by avoiding the 
use of EITHER and reverting fro the well behaved domain D N> or by assuring 
ourselves, at each application of EITHER, tfef the result is single valued. 
We may note, pursuant to the latter program/that for all expressions a. and b_, 
E[ (EITHER §,&)] is single valued if 

1) a. is single valued and b, is meaningless; or 

2) b_ is single valued and a. is meaningless; or 

3) a, and b_ are both meaningless; or 

4) §. and tare each single valued and their values are semantically 

So long as the arguments to EITHER satisfy the above criteria, EITHER is 
intuitively functional. For each function £ whose: definition invb Ives EITHER, 
we may then carefully define a domain of specification S f 'such that for 
arguments * from S f , E[(f x)] i3 sln&Xp ^^ «, ^ for example, show 
that our definition of WHICHFF in terms pf EITHER is functional over a domain 
of specification including the functions {FF }. 

This means of avoiding the semantic difficulties of EITHER may raise certain 
aesthetic objections. First, it places on us the considerable burden of 
having to construct domains of specification for each of a large class of 
functions, and the necessity of showing that each s«ch function is well 
behaved over its particular domain of specification. SecoftdAt rules out 

3-5.1 -57- 

consideration of algorithms for well behaved functions which have 
multiply-valued subexpressions. Consider, for an example of the latter 
limitation, the function f defined so that 

f[n] = 5, n=1 
5, n=2 
else undefined. 

Now, since f[1]=5 and f[2]=5, it is intuitively reasonable to claim that 
f[either[1 ;2]]=5; yet we cannot make such a claim unless we are willing to 
assign some semantic value to either[1;2]. 

3.5.2: EITHER and the Lambda Calculus 

There is an essential incongruence between EITHER and the axiomatic basis of 
the Lambda Calculus which precludes the incorporation of the former as a 
primitive with an associated delta rule. 1 Recalling that these axioms define 
an equivalence relation, =, on the domain of the language, incorporation of 
EITHER results in the equivalences: 

(EITHER 1 2)=1 
(EITHER 1 2)=2 
and hence 


from which it follows, by the famous logic of Russel, that "I am the Pope". 
Clearly the relation between (EITHER 1 2) and 1 is not equivalence, but rather 
some irreversible reducibility property. Any evaluator which can yield 1 as 
the value of (EITHER 1 2) cannot be claimed to preserve semantic equivalence; 
it merely reduces that expression to one of its several values and discards, 
in the process, information about the other values. This is the underlying 
reason why N (and the Lambda Calculus) are incapable of expressing WHICHFF, 
and is basic to the proof of Theorem 3.4. 

Such a delta axiom is formally ruled out by the requirement that the 
arguments to primitives be in reduced form, thus restricting applications of 
fc,±iHh,K to cases where both arguments have meaningful E values. 

-58- 3.6 

3.6: The Power Set Domain * 

The natural extension of a functional domain F of single-valued elements to a 
domain F* of multiply-valued elements involves the interpretation of F* as the 
Power set , or set of subsets, of F. Thus the elements 2 and 3 of F correspond 
to the unit subsets {2} and {3), respectively, in F*, while the semantic 
element of F* corresponding to the value of (EITHER 2 3) is the subset {2,3} 
of F containing both 2 and 3. The meaningless element * corresponds to the 
empty subset of F, having no value. Other useful relationships which we 
would like to see in F* include the following; 

1)- If s~b in F then {a_,bj~a~b in F». 

2) (EITHER (£&)(£ bj)~(£ (EITHER a_ b_) ), or equivalently, the elements 
{f[a],f[b]} and f[{a,b}] in F» are the 

3)The natural interpretation of either on functions leads to the semantic 
equivalence (EITHER f g)~(LANBDA(X) (EITHER (fX)(g X))). This allows us 
to propose, in symmetry with (2), that: 

H) ((EITHER £&) a.) " (EITHER (£ a_) Cga.)). 

5) (EITHER a. *)"&. where * is the element corresponding to the undefined 

6) If a. corresponds to {a , ...,a.} in F* and b_ corresponds to {b 1t ... ,b.} , 
then (EITHER a. b.) corresponds to {a..,...,a , b 1t ...,b.} in F*. In 
general, EITHER of multivalued elements corresponds to the union of the 
respective elements of F*. 

3.7: Interpretation of F* 

The semantic model being developed in this chapter demands a certain amount of 
intuitive realignment on the part of the reader. The attractive feature of F* 
as a semantic domain is that it allows the preservation of a notion of 
semantic equivalence, without cost in terms of expressibility of certain 
functions. Its major disadvantage, at least from an intuitive standpoint, is 
that it requires that we postulate certain abstract semantic elements which 

3.7 -59- 

are intangible in practice — if the expression x_ has multiple values, say 2 
and 3, then we have no way of discerning from the value "3" typed by our E 
interpreter that "2" is also a value of x. We could, of course, build an 
interpreter which would enumerate the values of x by dovetailing computations 
at each EITHER juncture. However, as x might have infinitely many values, 
this process may never terminate; worse yet, even for an x with finitely many 
values we cannot tell, in general, when all of the values have been typed. 

There are, however, situations where this ambiguity is unimportant. We may 
know, for example, that x is single valued, in spite of the dual values of a 
subexpression y_ of x_. Alternatively, we may recognise that x_ has many values, 
but be willing to settle for any one of them. 

3.8: Computable elements of F* 

If we have a procedure for identifying the computable elements of a single 
valued domain F, we can characterize the computable elements of the power set . 
domain F« as those elements of F» whieh are effectively enumerable sets of 
computable elements of F. Given an expression X we can enumerate the 
components of the F» element representing X; one means of doing so is provided 
in Chapter 6. Furthermore, given an expression G for a function which 
enumerates a set S of elements of F, we can construct an expression whose 
representative F* element is S; take for example the expression 

((Y (LAMBDA(H)(LAMBDA(X) (EITHER (G X) (H (PLUS 1 X)))))) 0) 

where Y is the fixed point operator (LAMBDA (Jf> ( (LAMBDA(G ) (F (G 

G) )) (LAMBDA (G) (F (G G))))). This expression reduces to an expression of the 


(EITHER (G 0) 

(EITHER (G 1) 

(EITHER (G 2) 

(EITHER (G 3) )))) 

and its corresponding element of F» is exactly the range of G. 

-60- 3.8 

We may use as our function G in the above expression an enumerator ENU of the 
entire domain F, constructed by the techniques of section; this 
expression, TOP, corresponds to the semantic element of F* which is the set F 

3.9: Summary 

This chapter raises the question of the expressibillty of a particular 
function, WHICHFF. This function is inexpressible £n the lambda calculus, and 
intuitively it requires a mechanism for multiprocessing for its implementation 
in spite of its applicative — hence time independent — nature. Two 
alternative extensions of the N interpreter are proposed, each of which 
renders WHICHFF expressible: 

1) Primitives can be added to N which allow coding and decoding of arbitrary 
expressions into and from numbers. This mechanism allows programs to 
access the representation of functions, and it is argued that such a 
CODE/DECODE facility extends any arithmetically complete language to 
functional completeness. Yet the use of this mechanism is awkward: the 
specific implementation of WHICHFF, for example, requires coding an 
interpreter which simulates the necessary multiprocessing. Moreover the 
semantic ramifications of CODE are drastic, involving abandonment of much 
of the applicative structure of any language in which it is embedded. 

2) A primitive, EITHER, can be added to N to implement multiprocessing. 
EITHER renders WHICHFF easily expressible, and it may be Justified 
semantic ally in an applicative language. 

In connection with (1), it is noted that although the new primitive CODE is 
radically nonfunctional, the inverse operation of DECODE (which maps codings 
into the functions which they represent) is acceptable as an element of our 
functional domain. A combinatory proof shows that such decoding functions 
are, in fact, expressible in the unmodified N language; hence we can write in 
the lambda calculi functions which enumerate the entire semantic domain of 
these calculi. 

3.9 _ 61 _ 

The introduction of EITHER or equivalent mechanism requires that we modify the 
structure of the semantic domain and its relation to expressions of a 
language. In particular, it seems most natural to associate with each 
expression a s^ of abstract values, rather than a unique single value. We 
thus move from the domain F of single values to the domain ?• whose elements 
are enumerable subsets of the elements of F; we term F* the power set domain. 

The presentation of EITHER in this chapter is informal and relies heavily on 
implementational notions such as multiprocessing. The following chapters 
formalize the mechanism in terms of systems of conversion rules, based on the 
lambda calculus; this process both Justifies and refines the rough 
implementation model sketched here. 

This empty page was substituted for a 
blank page in the original document. 

* -63- 

Chapter 4: 
Theories of EITHER-conversion 

While the implementation and semantic considerations of the previous chapter 
provide a strong intuitive basis for the interpretation of EITHER, the further 
development of this new mechanism requires something more concrete. 
Specifically, the incorporation of EITHER into a language E involves syntactic 
manipulations of expressions in E, and hence necessitates a formalism which 
distinguishes those syntactic manipulations which are semantically valid from 
those which are not. The relationships developed in the last chapter are 
analogous to the convention that "(PLUS 2 3)" represents the sum of 2 and 3, 
without a corresponding mechanism for associating this expression with the 
expression "5". 

This chapter begins the project of developing formalisms, i.e. conversion 
axioms, for the syntactic manipulation of expressions involving EITHER. 
Several theories (i.e., systems of axioms) are presented in this and 
subsequent chapters; each is based on the beta-delta 1 calculus, with 
additional axioms for manipulation of the new EITHER construct. The 
distinction between these theories stems from an issue of evaluation order, 
discussed in a following section, and reflects alternative interpretations of 
certain expressions involving EITHER. 

A principal difference between the axiom systems presented here and those of 
the lambda calculus is the introduction of a new asymmetry, in the form of an 
ordering relation >, between expressions of E. We have seen in previous 
sections that it is futile to require that E interpretation preserve an 
equivalence relation; such a requirement was shown to lead to an 
inconsistency in any language capable of expressing WHICHFF, since (WHICHFF 
FF 12 )~1 and (WHICHFF FF^)"2 together imply that 1~2. The asymmetry of >, 
however, allows the relations (WHICHFF FF^)^ and (WH ICHFF FF 12 )>2 to hold 
without compromising the semantic relation between 1 and 2. We view the 
relation > as designating EITHER-reducibility, and may interpret x>y 
informally to mean that the values of y are among the possible values of x. 


No attempt is made to incorporate eta conversion i 

»u duucmpu j.s maae to incorporate eta conversion into the svstems nppqpntpH 
here, although we expect that no new difficulties would arisfin doing so? 

-64- t 

We shall use x»y to mean that both x>y and y>x. 

It is important to distinguish between the relation » and the "reducible to" 
relation, ->, of the lambda calculus. If the expression X is reducible to the 
expression Y by means of conventional lambda calculus axioms, then it will 
follow that X>Y and Y>X; the reverse, however, is not true. The semantic 
interpretation of X>Y is that every value of Y is also a value of X; i.e., the 
element of F* corresponding to Y is a subset of the element corresponding to 

4.1: Preliminary Definitions 

The terminology of this section is adapted from standard usage in the lambda 
calculus, and appears e.g in Curry[12], 

The relation > defined in each of the axiom systems presented here is a 
monotone relation, i.e. it has the following properties: 

Reflexivity: For every X, X>X. 
Transitivity: If X>Y and Y>Z, then X*Z. 

Monotonicity: If X>Y and B is the result of substituting X for an occurrence 
of Y in expression A, then B»A. X for an occurrence of Y, then B>A. 

The above properties are assumed to be axioms of each system. 

Certain of the axioms to be presented lead to a distinction between the 
operations of contraction and abstraction : for example, the derivation of 
S[A;x;M] 1 from ( (LAMBDA(x)M)A), justified by the beta axiom of the lambda 
calculus, may be termed a beta-contraction. The inverse operation of 
converting S[A;x;M] to ( (LAMBDA(x)M)A) may be termed a beta-»abstractlon . An 
expression which is a candidate for contraction is called a redex : thus 
( (LAMBDA(x)M)A) is a beta-redex in the lambda calculus. The result of 
performing a contraction on a redex X is termed the contracture of X. 

An expression in a particular calculus is in normal form if it contains no 

Recall that S is the substitution operation of the lambda calculus, Defn 

4.1 -65- 

redex applicable to that calculus. We say further that the expression X is in 
beta-normal form if X contains no beta-redex, and similarly for the delta, *, 
and E redexes to be defined presently. The statement that X is in normal 
form, without further qualification, may be taken to mean that X contains no 
beta-, delta-, *-, , or E-redexes. 

We shall often use the notation X{Y} to designate an expression X containing a 
particular instance of a subexpression Y; having identified an expression 
with the notation X{Y}, we shall then use an expression of the form X{Z} to 
denote the result of replacing Y in X{Y} by the expression Z. In this 
notation, the monotonicity of > is the implication of X{Y}>X{Z} by Y»Z. 

A relationship of the form A>B is in general derived through a series of steps 
A 1 >A 2 , A 2 >A_, where each A.>A. .. involves the substitution of an expression Y' 
in A. for an occurrence of an expression Y>Y'. The monotonicity of > 
justifies each such substitution, and the transitivity assures that the 
validity of the entire series follows from the validity of the individual 
steps. We shall use the terminology 

Defn 4.1: A reduction step in A from X to Y, for expressions X and Y and a 

particular axiom system A, is a proof that X>Y by a single application of 
an axiom of A. 

Defn 4.2: A reduction sequence from X to X in system A is a series 

X »X.>...>X such that each X.>X. , is a reduction step in A. 
1 n i i+1 

4.2: The Either-R Theories 

The first axiom, common to each of the systems presented, is taken directly 
from the lambda calculus: 

Axiom alpha : (Renaming) Let E be an expression of the form (LAMBDA(X)A) where 
X is any variable and A is an expression, and let Y be any variable not 
occurring free in A. Then E«(LAMBDA(Y)S[Y;X;A]) . 

-66- n.? 

We say that expressions A and B are congruent if A can be converted to B by 
alpha conversion alone. Congruence is thus reflexive, symmetric and 
transitive, and to simplify subsequent proofs we shall often allow ourselves 
to treat congruent expressions as identical* 

The next axiom is a restricted form of the beta axiom of the lambda calculus, 
allowing beta conversion only on a beta-redex whose argument is in normal 

Axiom beta-R : (lambda conversion) Let E be an expression of the form 

( (LAMBDA(a_)bJc_) where e_ is &> normal form. Then E*E', where E' is the 
contract um SLcjssfcJ of E, 

The following axiom provides a paradigm for delta-conversion, the application 
of primitive functions to arguments in normal ffcrm. A particular calculus 
will have a family of delta rules, specifying the behavior of each primitive 
— e.g. the delta rule lor the primitive PLUS asserting the equivalence of 
(PLUS n ra) to n+m for all integers n and m. Of interest here is the general 
form of such rules: 

Axiom delta : Let E be an expression of the form (ill where A is a primitive 
function symbol and B is a normal form expression containing no free 
variables. Then E«E', where E' is the contractual of E derived from B by 
the (here unspecified) rules associated with A. 

We may term such an expression E a delta-redex . and the conversion of E to E' 
is a delta-contraction. Since the relation between E and E' is equivalence, 

the axiom provides also for the delta-abstraction of E' to E. 

We note that axioms alpha, beta-R, and delta define a lambda calculus under 
the equivalence relation w, no use has been made of the asymmetric relation 

We shall term an expression of the form (EITHER a 1 a-)- f where a, and a ? are 
arbitrary expressions, an E-redex . We treat the E-r«dex as a new syntactic 
construct, rather than attempting to classify EITHER as an added primitive 
function whose operation is specified by delta rules. In particular, we 
regard the restriction that arguments of primitive functions be in normal form 

4 - 2 -67- 

as unacceptable to the process of EITHER-conversion. 

Axiom epsilon : (EITHER-contraction) : If E is an expression of the form (EITHER 
a 1 a 2 ) where a 1 and a ? are expressions, then E>a.. and E>a 2 . 

Axiom mu: For every expression E, E-( EITHER E E). 

Axiom rho: (EITHER-distribution) If E is an expression of the form (f (EITHER 
a b)), where f, a, and b are arbitary expressions, then E-E' where E' is 
the expression (EITHER (f a)(f b)). 

The conversion of the redex (EITHER a., a,,) to one of the expressions a or a 
will be termed an E-contraction. The conversion of an expression E to (EITHER 
E E) will be called an E -abstraction . 

4.2.1: Properties of Either Theories 

The elementary relationships established in this section hold for subequent 
theories as well as for Either-R. In addition to their usefulness in proofs, 
they provide a preliminary reassurance that the Either-R axioms are consistent 
with the intuitive semantics of EITHER. 

Thm 4.3: X^Y if and only if, for all Z, 

Y>Z => X>Z 

Proof- only if: by the transitivity of >. 

if: Let Z be Y; then Y>Y by the reflexivity of >, hence X>Y by above 

The above theorem is consistent with the intuitive notion that X»Y means 
values derivable from Y are also derivable from X. 

Axiom mu justifies the trivial abstraction of an expression E to the 
expression (EITHER E E) ; The following theorem shows that nontrivial EITHER 
expressions may be abstracted: 



Thm 4.4: Let X, A, and B be expressions such that X>A and X>B. Then 

proof; By Axiom mu, X»( EITHER X X). 

But since X*A and X»B, (EITHER X X)>(EITHER A B) by the monotonicity of 
». Hence X»( EITHER A B). 

We may apply this theorem, for example, to the expression A given by 

A=.( (LAMBDA (X) (PLUS X3))(PLUS 1 2)) 
By performing single beta and delta contractions, repectively, on A we deduce 
the relations 

AXPLUS (PLUS 1 2) 3) 
A>( (LAMBDA (X) (PLUS X 3)) 3) 
Application of Thm 4.4 yields the result 

AXEITHER (PLUS (PLUS 1 2) 3) ( (LAMBDA (X(PLUS X 3)) 3)) 
This demonstrates that the Either-R theory allows EITHER-free expressions 
(such as A above) to be converted to expressions containing EITHER. 

Thm 4.5: X«Y if and only if for all Z, X>Z<=>Y>Z. 
proof : is by two applications of 4.3. 

Thm 4.6: For all f, g, and a, 

((EITHER f g) a)>(EITHER (f a)(g a)) 

Proof- By Axiom epsilon, ((EITHER f g) a)Mf a) and ((EITHER f g) a)>(g a); 
hence, by Thm 4.4, ((EITHER f g) a )>( EITHER (f a)(g a)). 

The intuitive arguments of the last chapter suggest that the above result 
could be strengthened to full equivalence (i.e., -) , and this more powerful 
result may in fact be a theorem in our Either theories; however we have not 
pursued this equivalence since it is irrelevent to the subsequent proofs. 

4.2.2 _69- 

4.2.2: EITHER and Evaluation Order 

Chapter 2 notes the distinction between normal and applicative order 
evaluation, characteristic respectively of the N and T interpreters. 
Applicative order evaluation, in which arguments to a function are evaluated 
prior to the application of the function, is shown in that chapter to lead to 
the inexpressiblity of certain functions which ignore their arguments. For 
example, the applicative order evaluation of the expression 

((LAMBDA(X)3) A) 
does not terminate if the value of A is undefined, whereas the normal order 
evaluation of that expression yields the value 3. 

The restricted conversion of the beta-R axiom is similar to applicative order 
evaluation — in each case, the argument to a function must be avaluated 
(reduced to normal form) before the application of the function (beta 
conversion). The only distinction between beta-R conversion and the 
applicative order of the T interpreter is the degree of evaluation required; 
while Either-R requires that arguments be reduced to normal form, T requires 
only that they be reduced to lambda expressions or atoms. We may thus, view 
the restriction on beta conversion as a more serious constraint than the 
applicative order evaluation of T. 

The motivation for this restriction in the Either-R system is our intuitively 
based demand that the axiom of EITHER-distribution, rho, hold. This axiom is 
in fact inconsistent with the unrestricted beta conversion of the lambda 
calculus; consider, for example, the expressions I, Z, and F defined by 

I =. (LAMBDA(X)X) 
Z = ( LAMBDA (Y) (LAMBDA (X)X)) 
F _= (LAMBDA (H) (H H) ) 

Using the axioms of Either-R (notably EITHER distribution) in conjunction with 
unrestricted beta conversion, we may deduce that I=Z as follows: By Axiom mu, 

I =. (EITHER I I) 

and by (restricted) beta abstraction on each of the terms of the E-redex, 

T = (EITHER (F I ) (F Z)) 

-70- 4.2.2 

since both (F I)=I and (F Z)=I. Then the axiom of EITHER distribution yields 

I =. (F (EITHER I Z)) 

from which, using unrestricted beta conversion (as the argument is an E-redex 
and hence not in normal form) we deduce that 

whence by EITHER contraction 

I > (I Z) = Z 
Thus we have derived I>Z; to show Z>I (and hence I.Z) we make the deductions 


(I Z) MZZ) 
Z > I 

using the raonotonieity of > and beta-R abstraction. 

It follows that, using unrestricted beta conversion in conjunction with the 
Either-R axioms* we can prove every pair of expressions equivalent — i.e. , 
the system is inconsistent. We avoid this pitfall it* Eifcher-R by means of the 
restriction on beta conversion. The beta-R restriction is not, however, the 
only solution to this problem, and in Chapter 7 an alternative axiom system — 
designated the Either-K theory — is presented. 

It should be noted at this point that the restriction on beta conversion is 
expensive in terms of expressive power. It prohibits, for example, the 
reduction of the expression 

((LAMBDA(X)3) ( (LAMB0A(Y)(I Y) KLAMBDA(Y) (I Y))) 

to the value 3, since the argument in that expression has no normal form. A 
more serious drawback is that it interferes with the expressibility of 
recursive functions since recursion requires, in the lambda calculus, the 
application of functions to arguments having no normal forms. Chapter 5 is 
devoted to the mechanism of *-conversion, which mitigate these limitations 
imposed by the restricted beta conversion. 

4.2.3 -71- 

4.2.3: Consistency of Either-R 

An extension of the axiomatic basis of the Lambda calculus may lead to 
inconsistencies, e.g. the equivalence of 1 and 2. Such equivalences do not 
hold in the conventional lambda calculus; in particular, the first Theorem of 
Church and Rosser establishes the consistency of the Lambda Calculus axioms by 
showing that the proposition X=Y is not provable for any pair of expressions X 
and Y having incongruent normal forms. We are thereby assured that the 
equivalence relation = established by the lambda calculus does not place every 
expression in a single equivalence class, and thus that the cardinality of the 
domain of the Lambda Calculus is greater than 1. The existence of infinite 
sets of mutually incongruent normal forms 1 shows that the domain of the lambda 
calculus is infinite. Moreover, an important theorem of Boehm[20] shows that 
any axiomatic assertion of the form X=Y, where X and Y are incongruent normal 
forms, leads to an inconsistency. 

The theorems of Church-Rosser and Boenm are, not surprisingly, inapplicable to 
the axiomatic extension presented here. Furthermore, they probably cannot be 
augmented in minor ways to argue the consistency of the present system, as the 
uniqueness of normal forms, on which they depend, has been compromised by our 

Accordingly, is the purpose of this section to establish that the domain of 
the lambda calculus is a subset of the domain of the Either-R system, and that 
the new equivalence relation • is consistent with the relation = of the lambda 
calculus. In particular we wish to show that, for any two either-free 
expressions X and Y, X=Y if X-Y. Proof of this assertion establishes that 

1) The domain of the Either-R system includes the domain of the lambda 
calculus, hence the new system is nontrivial (having infinite 
cardinality); and 

2) The semantic equivalence defined by the Either-R calculus, applied to 
EITHER-free expressions, is a subset of the equivalence of the lambda 

ete° r exaraple « the set 1= (lambda (x)x), I '=.( lambda (x)I ) , I"=.(lambda(x)I ' ), 

-72- 4.2.3 

It has been noted that in the Either-R system there are expressions X and Y 
such that X=Y but for which X-Y is not provable ~ a consequence of the 
restriction on beta conversion which is explored further in the analysis of 
the R-» system in the following chapter. 

We precede to the consistency proof, beginning with with the following 

Defn 4.7: The EITHER-free expression X' is an e^gaidlia of the expression X 
if and only if X' nay be derived from X by replacing every e-redex 
(EITHER Xj x 2 ) in X by one of the operands x, or x , 

Thus the expression X' is an e-residue of X if X' is EITHER-free and X>X' may 
be demonstrated solely by means of EITHER-contraction (axiom epsilon). 

Defn 4.8: The expression X is uMtao. if and only if there exists some 

EITHER-free expression Y such that, for every e-residue X' of X, X'=Y (in 
the lambda calculus). 



is unitary, since its e-residues (LAMBDA(X)X) and (LAMBDA(Y)Y) are congruent. 
We note that EITHER-free expressions are unitary, although unitary expressions 
are not necessarily EITHER-free, as the above example demonstrates. 
Furthermore, a unitary expression X may contain subexpressions which are not 
unitary; witness the expression 

( (LAMBDA (X) (DIFFERENCE X X))(EITHER 2 3)) [4.9] 

whose e-residues are 



each of which is convertible to by the rules of the Either-R system. Hence 
expression [4.9] is unitary; it contains, however, the subexpression 

(EITHER 2 3) 

4.2.3 -73- 

which has e-residues 2 and 3, which are not equivalent under =. Hence the 
subexpression is not unitary. 

The proof of the consistency of Either-R is based on the observation that, 
while EITHER may be introduced into EITHER-free expressions by 
EITHER-abstraction, the result is necessarily unitary. Moreover, the axioms 
of Either-R preserve the unitary nature of expressions; we will thus argue 
that the result of an Either-R reduction sequence on an EITHER-free expression 
must be unitary. We now introduce a relation which orders expressions by the 
interconvertability , in the lambda calculus, of their e-residues: 

Defn 4.10: For any expressions X and Y we say that X encloses Y if, for every 
e-residue Y' of Y, there is an e-residue X' of X such that X'=Y' in the 
lambda calculus. 

Observe that enclosure is reflexive and transitive; the following lemma 
establishes that it is monotonic: 

Lemma 4,11: Let Y be a subexpression of X{Y} and let Y enclose Z. Then X{Y} 
encloses X{Z}. 

proof : Each e-residue of X{Z} is of the form X'{Z'} where Z' is an e-residue 
of Z; and for each e-residue Y' of Y there is a corresponding e-residue 
X'{Y'} of X{Y}. Hence for each e-residue X'{Z'} of X{Z} there is an 
e-residue X'{Y'} of X{Y} such that Y'=Z"; it follows that X'{Y'}=X'{Z'} 
hence X{Y} encloses X{Z}. 

Corollary 4.12: If X{Y} is unitary and Y encloses Z, then X{Z} is unitary and 
every e-residue of X{Z} is convertible to an e-residue of X{Y}. 

Lemma 4.13: Let X>Y be a single reduction step in Either-R. Then X encloses 



proof : Let U be the subexpression of X which is replaced by an expression W 
in the reduction step X»Y. By Lemma 4.11, we need only to show that U 
encloses W to establish that X encloses Y. We exhaustively examine the 
possible reduction steps from U to W: 

Case 1: Alpha conversion on U. Then U and W are congruent, and for each 
e-residue W' of W there is a congruent e-residue U" of U. 

Case 2: beta-R conversion on U. Let P be a beta-redex of the form 

( (LAMBDA (X)M{X})A) where A is in normal form, and let Q be the eontractum 

S[A;X;M{X}] of P. Then every e-residue P' of P is of the form 

( (LAMBDA (X)M'{X})A) where M'{X) is an e-residue of M{X} , and there is one 

such e-residue P' for every e-residue M' of M. Each e-residue W of W is 

of the form M'{A} and there is one such e-residue W for each e-residue M' 

of M. For each M' the corresponding e-residues of P and Q are 

( (LAMBDA (X)M'{X}) A) and M'{A) respectively, which are interconvertible in 

the lambda calculus by a single beta conversion; hence P encloses Q and Q 

encloses P. W is either a beta-R contraction or a beta-R abstraction of U, 

hence U encloses M. 

Case 3: delta-conversion on U. If either U or W is a delta redex, then both U 
and W are EITHER-free and thus U encloses W. 

Case 4: EITHER contraction. If U is an expression of the form (EITHER A^ ^ 
clearly U encloses both A 1 and A ? ; each e-residue of W is an e-residue of 
A. or of Ap. 

Case 5: EITHER-abs tract ion. Then W is of the form (EITHER U U), and each 
e-residue of W is an e-residue U" of U. 

Case 6: EITHER-diatribution. Let P be an expression of the form 

(EITHER (F A)(F B)) 

and let Q be 

(F (EITHER A B) ) 
The e-residues of P consist of all the expressions of the forms (F' A') and 
(F' B') where F', A', and B' are respectively e-residues of F, A, and B. 
We note that the e-residues of Q consist of exactly the same set of 
expressions, hence P encloses Q and Q encloses P. Thus for a conversion 

4.2.3 _ 75 _ 

U>W of the forms ?>Q or Q>P, U encloses W. 
This completes the proof of Lemma 4.13. 

We present the obvious generalization of this result 


Corollary 4.14: Let X and Y be expressions such that X>Y in the Either-R 
system. Then X encloses Y. 

£rpof follows directly from Lemma 4.13 and the transitivity of the enclosure 

This corollary shows that the ordering > of the Either-R system implies 
enclosure; thus the number of distinct (under = of the lambda calculus) 
e-residues of an expression X can only be decreased by a reduction step in 
Either-R. While each reduction step may introduce new E-redexes (by 
EITHER-abstraction), the terms of each redex so introduced are necessarily 
interconvertable. The consistency of the Either-R theories is a special case 
of this corollary: 

Thm 4.15: Let X and Y be EITHER-free expressions such that X>Y in the 
Either-R theories. Then X=Y in the lambda calculus. 

erpof: By Corollary 4.14, X encloses Y; since X and Y are each EITHER-free, 
X and Y are respectively e-residues of X and Y. Hence X=Y in the lambda 

The above theorem establishes that the Either-R theories are consistent in the 
sense that they introduce no new equivalences between expressions which are 
distinct in the lambda calculus; and are hence of infinite cardinality. It is 
noteworthy at this point that the above proof, specifically Lemma 4.13, 
depends on our restriction on beta conversion, when unrestricted beta 
conversion is allowed (as in the Either-K theories presented in Chapter 7) it 
is not true in general that every beta-redex X encloses its contractum X', as 
demonstrated by the beta redex 

.76- 1-2.3 

A= ( (LAMBDA (X) (PLUS X X))(EITHER 2 3)) 

whose e-residues are each convertible to 2 and 3, respectively, while the 
contractual of A 

(PLUS (EITHER 2 3) (EITHER 2 3)) 

has an e-residue (PLUS 2 3) which is convertible neither to 2 nor to 3. 

4.3: Summary 

This chapter defines the ground rules for the axiomatization of Either 
theories and presents the Either-R theory. fRiile the usefulness of this 
system is limited due to the restriction placed on beta conversion, it 
develops much of the mechanism to be used in subsequent chapters. 

The principal distinction to be made between the Either theories lies in the 
circumstances in which beta-conversion is allowed. The Either-R Theories, 
which prohibit beta-conversion unless the argument to be substituted is in 
normal form, allow the distribution of functions over the terras of an 
EITHERexpression - a relationship which we find intuitively gratifying. 
Unfortunately this restricted beta-conversion results in a very weak theory, a 
problem to which the next chapter is devoted. 

The Either-R theory presented in this chapter is shown to be consistent in the 
sense that X»Y, where > is the ordering defined by the new axioms, is not a 
tautology. The proof is based on the consistency of the lambda calculus; 
specifically, it is shown that, for expressions X and Y which are EITHER-free 
(and thus admissible syntactically in the lambda calculus) X>Y implies the 
interconvertability of X and Y. This general technique will be followed in 
subsequent consistency proofs as well. 

5 _77- 

Chapter 5: 

It was noted in the previous chapter that the restricted lambda conversion of 
the beta-R axiom, i.e. the requirement that the argument of a beta-redex be in 
normal form before the contraction of that redex, severely limits the 
expressive power of languages based on the Either-R theory. In particular, 
the inexpressibility of recursive functions constitutes an intolerable 
restriction since it renders such languages functionally incomplete. 

The mechanism of *-conversion, to be introduced in the present chapter, 
ameliorates this limitation by extending the ordering relation > in a way 
which is consistent with its function in the Either-R theory. Although 
•-conversion and EITHER reduction are in an important sense complementary 
operations, their respective mechanics may be dealt with separately; thus for 
the purposes of this chapter we temporarily disregard the axioms of EITHER 
conversion. In Chapter 6 we combine the two mechanisms. 

The semantic interpretation of > suggested by the Either-R theory is one of 
inclusion gf values; it was noted that X»Y signifies, in general, that each 
value of Y is also a value of X. The corresponding relation in the semantic 
domain F* is set theoretic inclusion. Thus if x and y are the semantic 
elements of F« corresponding to X and Y, respectively, then X>Y implies that y 
is a subset of x. Consistent with the semantic notions of Chapter 3, the 
expression (EITHER X Y) corresponds in F» to the union of the elements x and 
y. It was further suggested that the undefined computation corresponds, in 
F«, to the empty set — i.e., it has no values whatsoever. 

This chapter develops the syntactic analog of the empty set in F*. 
Specifically, the new syntactic element « is introduced as the canonical 
normal form representation of the undefined computation. The interpretation 
of > as set theoretic inclusion in F* suggests that, for every expression X, 
X»« (since every' set has the empty subset). It would seem, then, that the 
consummation of the semantics of EITHER reduction requires that its syntactic 
mechanism reflect this aspect of the structure of F*. 

-78- 5.1 

5.1: The R-* Theories 

We now focus our attention on "-conversion and its relation to the restricted 
beta conversion. To this end we consider the R-* system whose axioms include 
alpha* beta-B, and delta discussed previously, in addition! to the following: 

Axiom sigma : ( "-contraction) : For every expression E» E»*. 

Thus * is an expression in the R-» system which Is lower, in the sense of >, 
than every other expression:, ttiile every/ expression; is reducible to *, * is 
itself only reducible to * Cas * is not a beta- or delta-redex, and contains 
no variables). 

Defn 5.1: An expression of the form C* A), where A is an arbitrary 
expression, is called a * -redex . 

Consistent with our previously defined notion of normal forms, we shall 
henceforth require an expression X to contain no *-redexes if it is in normal 
form. Hoting that the only conversion which may be performed on a *-redex 
without resulting in another *-i>eAex is its replacement by *, we shall say 
that the con trac turn of a *-redex is *. 

5.1.1: Significance of normal forms 

The restricted lambda conversion allowed by the beta-R axiom bears a curious 
resemblance to the lambda-I calculi of Churchill. In these systems, Church 
specifically prohibits expressions of the form CLA*®JA(X)M)S unless the 
variable X appears free ia the body Wj thus the lambda-I systems exclude, in 
general, functions which ignore their arguments. A principal consequence of 
this restriction is the fact that, for expression X to have a normal form, 
every subexpression of X must have a normal form, le note, with passing 
interest, that the normal fbrm restrictis* of hefta-B allows us to derive any 
normal fbm in the lambda-I calculus which is possible using unrestricted beta 
conversion; this follows from the observation that in the lambda-I system we 
can always reduce the argument in a bsta-reoex to normal form before 
contracting the redex. 

5.1.1 -79- 

Church's preference for the lambda-I over the unrestricted "lambda-K» 1 
theories stems from the elusive nature of those expressions having no normal 
forms. The theorem of Boehm assures us that expressions having incongruent 
normal forms are semantical ly distinct, and the theorems of Church-Rosser 
guarantee that equivalences between expressions having normal forms are 
decidable. The semantics of normal forms is consequently uncomplicated: 
every pair of semantically equivalent normal form expressions is provably 
equivalent, and for every pair of incongruent normal forms we can find a 
context in which they produce different values. 

The admission of expressions having no normal forms compromises this situation 
severely. The requirement that a semantic equivalence relation be 
exfrensional , i.e. that equivalent expressions produce equivalent values in 
identical contexts, leads tea distinction between semantic equivalence and 
the equivalence of interconvertability under the lambda calculus. Scott[22], 
for example, demonstrates an infinite sequence Y, Y ... of fixed point 
operators which are not convertible to one another despite the fact that they 
produce the same values when embedded in identical contexts. The problem of 
constructing a functional domain for the lambda calculus is fundamentally 
equivalent to the definition of an extensional relation of semantic equialence 
over the expressions of that calculus, a project whose recent success is due 
to Scott. The technique used by Scott[5,6,22] involves the notion of 
successively better approximations to the abstract semantic element 
represented by an expression X, so that the semantic element associated with X 
becomes the limit of this sequence of approximations. In the Scott model, a 
function f approximates every extension f of f'; more generally, f ' 
approximates f if and only if for every z, f'[z] approximates f[z]. This 
notion of approximation seems essential to the interpretation of domain 
elements as functions, largely because the theories of functions with which we 
are familiar employ type restrictions ruling out self-application. 2 

r.-nSJ^f^Il2i a ? d 'Sir ryC , 12] , ref er to the unrestricted conversions of the 
2rtSyt2fh?i n fi tam £da calculus as lambda-K conversion, presumably because of the 
I is SSiiJS f2L t ?L COHlb i n ? fc ? r . K f- ( 45P^ (X)( fe AMBDA ^> x >) in t^se systems? 
boSd^S^W& r b^ of the 

fhi n ;^.^Ti ieu i a rt < LA «fDA(X)(X X)) is difficult to interpret as a function in 
fSotiSl K^r 1 ^"?' Hindley[21] speculates that a theory of 
n™Si?2Si-i ) 5 se ?i 0n com 5inatory logic, rather than set theory, might 
?2SiS SSiListS self - a PP llcati °"; while awaiting further developments we 

-80- 5.1.1 

The mechanism of "-conversion presented in this chapter is reminiscent of the 
Scott construction. Specifically, we introduce means by which the various 
approximations of an abstract semantic element can be represented as 
expressions in the language itself, and provide for the syntactic conversion 
of an element X to an approximation X' of X. We have thus come to view 
"-conversion as a syntactic analog of the Scott construction in which 
approximations are expressed in the domain of the language rather than in the 
abstract semantic domain. 

The addition of *-conversion to the lambda calculus leads to a multiplicity of 
normal forms for every expression. We shall see, for example, that the Y 


which has no normal form in the conventional lambda calculus, has infinitely 
many normal forms 

(LAMBDA(F)(F *)) 

(LAMBDA(F)(F (F *))) 

(LAMBDA(F)(F (F (F »)))) 

when •-conversion is admitted. Each of these normal forms may be interpreted 
as an approximation to the Y operator, and in any context where Y gives a 
normal form value, one of the above normal forms of Y will give an identical 
value. Since the semantic element associated with each of these normal forms 
is clear (in the sense that normal forms are semantically distinct) we retain 
something of the semantic simplicity of the lambda-I calculus. The semantic 
value of a given expression is simply the set of normal form values of that 
expression, and expressions X and Y are semantically equivalent if and only if 
they have identical sets of normal forms. 

One of the motivations for •-conversion is to enable us to retain the power of 
the unrestricted (lambda-K) calculus while restricting beta conversion. It is 
intuitively reasonable to expect that one can always find a sufficiently close 
approximation to the argument of a lambda expression that the restriction on 

5.1.1 -81- 

beta conversion becomes unimportant where '-conversion is allowed, and much of 
the remainder of this chapter is devoted to the proof that this is in fact the 

5.1.2: Theorem on Normal Forms 

The main result of this section sheds light on the ordering (under » of the 
normal forms derivable in «-» from an expression It. We begin with the 
following definition, adapted from Curry[12]: 

Defn 5.2: Let P be a redex and Q be a subexpression in an expression B, and 
let B' be the result of replacing P by its contractual P' in B. We define 
the residues £f_ fl with respect to. P as subexpressions of B' designated 
as follows: 

Case 1: P and Q are the same redex in B. Then Q has no residual with 
respect to P. 

Case 2: P and Q are non-overlapping subexpressions of B. Then the 

residual Q' of Q is that subexpression in B' which is homologous 1 to Q 
in B. 

Case 3: P is a subexpression of Q. Then the residual of Q in B' is the 
expression Q' which is homologous to Q in B. We note that the 
occurrence of P in Q has been replaced by P' to make Q'. 

Case 4: P is a beta-redex ((LAMBDA(X)M)A), and Q is a subexpression of A. 
Then P' is S[A;X;M] and contains n instances of A corresponding to the 
n free occurrences of the variable X in M; let these instances of A be 
identified as A ( ... A R . Each Ai contains an instance Qi of the redex 
Q; these n expressions Q^ ... Q Q are the n residuals of Q in B'. Note 
that n may be zero, in which case we term the contraction of P a 
cancellation and Q has no residuals. 

homologous subexpressions occupy the same relative position in their 
containing expressions; thus A in ((X (HA) Z) Y) is homologous to B in ( (P (Q 
n r independently of the structure of the subexpressions X, W, Z, Y, P, 

W i Hj a no o« 

-82- 5.1.2 

Case 5: P is a beta-redex ( (LAMBDA(X)M)A) and Q is a subexpression of M. 
Then P" is S[AjX;M] and the residual Q' of Q is the subexpression of 
P* which is homologous to Q in M. 

Case 6: P is not a beta-redex, and Q is a subexpression of P. Then Q has 
no residual in B*. 

Informally, a residual of an expression Q is an image of Q after a 
contraction. Consider, for example,, the residuals of the subexpression (PLUS 
3 *) in the beta-redex 


whose contractus is the expression 

CPLBB CPLHS 3 *>(PUB 3 *>> 

We note that the two residuals of the subexpression (PUB 3 4) of expression 
[5.3} are the occurences of CPLBS 3 *) in the eontractum. Contraction in the 
delta redex (PUB 3 ' *> in empreasios [5.31 yields the residual 


We shall occasionally find it useful to speak of the residual of an expression 
Q after a series of contractions; we amy thus refer to Q as a resldal of Q 

with respect to the sequence of contractions B£& >...>B if there is a 


subexpression C^_ t of B^-t such that Q^ is a residual of Q and C^ is a 
residual of $». Thus consecutive beta- and delta-contractions on expression 
[5.3J yield 

(PLUS 7 (PUS 3*)) 

which contains a single residual of the subexpression (PLQS J t). The 
following leans establishes that, the residual of a redex is always a redex: 

Lemma 5.4: Let P and Q be red exes in an expression B t and let Q* be a 
residual of Q with respect to P. Then Q' is a redex. 

proof: we consider the following collectively exhaustive cases: 

5.1.2 -83- 

Case 1: P and Q are non-overlapping. 1 Then Q' is the same redex as Q. 

Case 2: P is a subexpression of Q; we consider the cases of the syntax of 

a) Q is a beta-redex of the form ((LAMBDA(X)M A). If P is a 
subexpression of M, then Q' is the beta-redex ((LAMBDA(X)M')A). If 
P is a subexpression of A, then Q' is the beta-redex 

( (LAMBDA (X)M)A'). 

b) Q is a »-redex of the form (• M); then P must be a subexpression of 
M, and Q' is the «-redex (* M'). 

c) Q cannot be a delta-redex, as it contain P. 

Case 3: Q is a subexpression of P; we consider cases of the syntax of P: 

a) P cannot be a delta-redex, as it jontains the redex P. 

b) P cannot be a »-redex, as then Q would have no residual. 

c) P is a beta-redex of the form ( (LAMBDA (X)M) A) where Q is a 

. subexpression of A. If Q is cancelled by the contraction of P, then 
Q has no residual; hence M must contain 1 or more free occurrences 
of X. Then each residual of Q is the redex Q itself. 

d) P is a beta-redex ((LAMBDA(X)M)A) where Q is a subexpression of M. 
We examine syntactic cases of Q: 

i) Q is a delta-redex; then Q' is identical to Q, since Q may 
contain no free variables (in particular, no free occurrence of 

ii) Q is a *-redex (* M). Then Q' is the »-redex (« M'). 

iii) Q is a beta-redex ( (LAMBDA(Y)B)C). Then Q' is a beta-redex of 
the form ( (LAMBDA (Y)B' )C'). 


othe"r. eXPreSSi ° nS are "^-overlapping if neither is a subexpression of the 

-84- 5.1.2 

The converse of the above lemma is not in general true, i.e., the residual P' 
of P may be a redex even though P is not. Consider for example the expression 

P a. (((LAMBDA(X)(LAMBDA(Y)Y)) 3) 4) 

which is not a redex. Contraction of the beta-redex in P yields the residual 
P' of P given by 

P' =. ((LAMBDA(Y)Y) 4) 

which is a beta-redex. 

We should like to distinguish between reduction steps in R-* which are 
contractions and those which are abstractions; for this distinction the 
following notation is convenient: 

Defn 5.5: A contraction step A»>B is a single reduction step from A to B 
which is either a beta-, delta-, or '-contraction. 

Defn 5.6: A contraction sequence A () »A 1 »...»A n from A Q to A n is a reduction 
sequence from A. to A containing only alpha-conversions and contraction 
steps. The length n of such a sequence is the number of contraction 
steps in the sequence. 

We now examine contraction sequences which terminate in normal forms 
beginning with 

Lemma 5.7: Let X{Y} be an expression containing a redex Y, and let 

X{Y}>>. ..>>X' be a contraction sequence of length n, where X' is in 
normal form. Then there is a contraction sequence X{Y'}>>. ,.>>X', where 
Y' is the contractum of Y, of n or fewer steps. 

proof is by induction on n. 

basis n=1: X' contains no redex, hence Y must be either contracted or 
cancelled (by a beta- or *-contraction). If Y is contracted then 
X[Y']»>X' by the null sequence. If Y is cancelled then X[Y']>>X' by the 
same contraction as X[Y]»>X'. 



induction: We assume the lemma to be true for sequences containing n or 
fewer steps. Consider the first contraction step X[Y]»X in the 
n + 1-step sequence X[I]»„.»x' f and let Y r .. Yj be the j 1 residuals of Y 
in X r If j=o then the argument in the basis applies, as Y is either 
contracted or cancelled in the first step. If j>0, j applications of the 
induction hypothesis establish that X, '»...»!' in n -1 or fewer steps, 
where X 1 ' is the result of contracting each Y i in X,. But X[Y']»X ' in 
a single step; hence X[Y']»X' in n or fewe/steps. 

The significance of Lemma 5.7 is that the contraction of a redex Y in 
expression X cannot pxfllflaa the reduction of X to normal form. Informally, we 
expect that if the subexpression Y plays a significant role in the evaluation 
of X, the contraction of Y will shorten the reduction of X; if, however, Y is 
irrelevent to the value of X then Y may be replaced by an arbitrary expression 
with no effect on the evaluation of X. This consideration motivates 

Lemma 5.8: Let B^B^. . ,»B n be a contraction sequence of length n, and let 
B n be in normal form. Let P be a redex in B Q , and let P' be the 
contractum of P. Then one of the following applies: 

a) There is a contraction sequence B*»...»B n of n or fewer steps, where 
B« is the result of substituting * for P in B ; ojl 

b) There is a contraction sequence B'»...»B n containing fewer than n 
contraction steps, where B' is the result of replacing P in B by P'. 

praoX is by induction on the length n of the contraction sequence B„»B . 


bgsis. n=1 ; then B »B n in a single contraction step. Let Q be the redex 

contracted in B Q »B n . If Q i3 the same redex as P, then B' is identical 

to B n , and (b) is satisfied. Otherwise P must have no residual in B , 

since B n i s in normal form and any residual of P is a redex. Then P^ust 

be cancelled by a beta- or '-contraction in B Q »B n , and (a) is satisfied. 

induction : n>1. Consider the redex Q contracted in the step B » B . if 
Q is the same redex as P, then (b) is satisfied as before. Otherwise we 
consider the J residuals P r .. Pj of P in B,. If j. then P is cancelled 

-86- 5.1.2 

in the step B^B^ and (a) applies. If j>0, we apply (by the inductive 
hypothesis) the lemma to the contraction sequence B.j». ..»B n , whose 
length is n-1 : 

Case 1: Each residue Pi in B 1 is convertible to •; i.e., (a) applies to 
each Pi. Then (a) applies to P in B Q , as B*»B 1 * in a single step, 
where B» is the result of replacing each Pi in B 1 by *. 

Case 2: Some residue Pi of P in B is not convertible to *; i.e., (b) 

applies to Pi. By Lemma 5.7, contracting any P R in B 1 cannot prolong 

the sequence B t >>. ,.»B ; by the induction hypothesis, there is at 

least one P^ whose contraction shortens the sequence. Then if B ' is 

the result of contracting each P in IL t there is a contraction 

sequence B„>>. ..>>B in fewer than n*1 steps. Since B'»>B ' in a 
l n « 

single contraction step (of the same kind as BQ»B.,)"(b) is satisfied. 
This completes the proof of Lemma 5.8. 

The following theorem establishes a fundamental property of »-conversion. 
Informally it ensures that, for any two normal form expressions A^ and A 2 » 
which are each derivable from an expression A, there is an expression A* in 
normal form which is an upper bound of A^ and k£ in the sense that A'^A,' 
and A*»A *, and furthermore that A»A*. This result is then extended to the 
case of an arbitrarily large finite set of expressions A 1 *...A n each derivable 
from A. The existence of normal form upper bounds of arbitrary sets of 
expressions derivable from A is essentially equivalent to the proposition 
that A can be approximated, to arbitrary accuracy, by normal forms derivable 
from A. 

Thm 5.9: Let A* and k* be normal form expressions and let A be any 

expression such that A»A • and A»A *. Then there exists an expression 
A* in normal form such that A»A*, A**^*, and A*»A 2 «. 

proof : Let P[n;m] be the proposition that Lemma 5.9 is true for every A, 

A * and A J* such that: 

(i) A»A • in n., steps and A»A 2 * in n 2 steps, where n^^n; and 
(ii) A contains m or fewer redexes. 


5.1.2 -87- 

Then the lemma is true if and only if P[n;m] is true for all n and m; we 
procede in the following steps: 

1) For every n, P[n;0] is true since in these cases A contains no redex 
and is consequently in normal form. 

2) For every m, P[1;m] is true since in these cases either A=A » or 
A=A •; hence A must be in normal form and A*=A. 

3) If for some n and m and for all j P[n,j] and P[n+1;m] are true, then 
P{n+l;m+l3 is also true. 

proof : Let A, A*, and A * be expressions such that the premises of 
P[n+1;m+1] are satisfied; then A contains m+1 or fewer redexes, and 
n^n^n+l wner€ n i and n o are tne res P* et < ive lengths of the sequences 
A»>A • and A*>k*. We now choose an innermost redex Y of A, i.e. a 
redex Y which contains no other rede:. Such a redex Y must exist 
unless A is in normal form, which is ruled out because m+1>0. Let 
A{Y} denote A (which contains Y as a subexpression) and let Y' be the 
contractum of the redex Y. Then by Lemma 5.8, one of the following 

a) Af*}*^* in n^ or fewer steps, and A{*}»A 2 » in n_ or fewer 

b) A{Y'}>>A * in n ' steps and A{Y'}>A * in n„' steps, where 
n 1 *+n 2 '<n 1 +n 2 . 

If case (a) applies, then A{M has fewer than m+1 redexes, and by 
P[n+1,m] the proposition P[n+i,m+1] is true. If (b) applies, then 
P[n+1,m+1] is true if P[n;j] is true (where j is the number of redexes 
contained in A{Y'}); by hypothesis, P[n;jJ is true for all j, hence 
P£n+1 ;n+1 ] is true. 

4) If for all j P[n;j] and P[n+1 ;03 are true, then for all i P[n+1,i] is 

proof is by induction on i. P[n+1 ;0] follows directly from (1); 
P[n+1;i+U follows from (3) and P[n+t;i]. 

-88- 5.1.2 

5) For every i and j, P[i;j] is true. 

proof is by induction on i. 

basis ; from (2), P[1 f j] is true for all j. 

induction : Assume that P[i;j] is true for all j. By (1), P[i+1 ;0] is 

true; hence by (4), P[n+1;jJ is true for all j. 

This completes the proof of Theorem 5.9. 

The proof of Theorem 5*9 involves a succession of steps from the expression A 
to the normal form A*, such that the result A of each step retains the 
property that A >>A^» and A.»A 2 *. The moderate complexity of the proof stems 
from the obscure sense in which each step comes "closer" to A*; by Lemma 5.8, 
each successive step from A to A. - either: 

i) Reduces (by one) the number of redexes, while keeping the total number 
of steps in the contraction sequences A.»>A..» and A,»A 2 * constant; oji 
ii) reduces the total number of contraction steps, while changing 

(increasing or decreasing) the number of redexes by some arbitrary finite 

The proof of Theorem 5.9 is essentially a demonstration that A* can always be 
derived from A by such a sequence in finitely many steps. 

The generalization to arbitrary finite sets of normal forms follows naturally: 

Corollary 5.10: Let A be any expression and let A... .A, be expressions in 
normal form such that, for each i, A>>Ai. Then there exists an 
expression A 1 in normal form such that A»A* and, for each i, A*>>Ai. 

proof is by induction on j. 

basis : For j>2, the corollary is trivially true; for j=2, it is true by 
direct application of Theorem 5.9. 

induction : Assume the corollary is true for each set A....Ak containing 
fewer than J expressions. By Theorem 5.9, there is an expression A 2* in 
normal form such that k.2*»k^ and A.,2»>>A 2 and A>>A T 2*; by the induction 
hypothesis, we can now find an upper bound of the set A 2*, A3,..., A 

5.1.2 -89- 

which contains j-1 expressions; let A* be the normal form upper bound of 
this latter set. But, since k*»k^2*, it follows that A*»>A 1 and A>>A 2 ; 
hence for each Ai, A*>>Ai, and A* is the required upper bound. 

The final theorem of this section establishes that, for the evaluation of any 

particular expression X{Y} (i.e., the reduction of that expression to a normal 

form) there exists a sufficiently good approximation Y* of Y such that Y* is 
in normal form: 

Thm 5,11: Let X{Y}>>. . .>>X* be a contraction sequence of length n, where X* 
is in normal form. Then there exists an expression Y* in normal form, 
such that Y»Y« and X{Y«}»X». 

proof is by induction on the length n of the contraction sequence. If n=0, 
then Y is in normal form and is the required Y». If n>0, we consider the 
residuals Y.....Y. of Y in X.. By the induction hypothesis each Y. can be 
contracted to a normal form Y » and the result X * of replacing each Y. 
in X 1 by If is such that X^^X*. Since for each i Y»Y i «, by Corollary 
5.10 there is a Y« such that Y»Y« and for each i Y*»Y . Then 
X{Y}»X{Y«}»X 1 ». ..»X». 

We may speculate further on the structure of the set S of normal forms of an 
expression A. The above theorem shows that any finite subset of S has an 
upper bound in S; since * is in S, we may claim further that each finite 
subset in S has a lower bound in S. It seems likely that S forms a lattice 
ordered by >, which is to say that each finite subset of S has both a least 
upper bound and a greatest lower bound. In general such a lattice of normal 
forms can be complete only for those expressions which have normal forms in 
the lambda calculus. 

5.1.3: Relation to the Lambda Calculus 

In this section we demonstrate a sense in which the R-* theory is as powerful 
as the (unrestricted) lambda calculus; , in particular, we show that any 
expression A which has the normal form A' in the lambda calculus has the same 

-90- 5.1.3 

normal form in R-*. 

Thm 5.12: Let A-->A„->. . .->A be a sequence of beta- and delta-contractions 
1 n 

in the Lambda calculus (possibly intermixed with alpha conversions), and 

let A^ be in normal form. Then A A »A in R-*. 
n On 

proof is by induction on n, the number of contractions in the sequence 

A n ->...->A . 


basis n=0; then A and A are identical, and the theorem is trivially 

induction ; n>0; we assume then that A.>>A and must show that A >>A Q . We 
procede by showing that A »A,. for each of the possible contraction steps 
A ->A... If the contraction step is an alpha- or delta- conversion, then 
the same contraction can be performed in R-* hence A.»A 1 ; we thus need 
only consider the case where A ->A 1 by a beta contraction. Let P be the 
beta-redex contracted in the step A ->A..; then P is of the form 

((LAMBDA(X)M{X}) Y) 

and the contracture P' of P is of the form M{Y}, containing j instances 
(residuals) Y.....Y of the argument Y. By Theorem 5.1 1 each Y t may be 
contracted in R-* to a normal form Y^, such that A.,»>>A n where A^ is 
the result of replacing each Y ± by Yj*. By Corollary 5.10 there exists 
an upper bound Y* such that Y»Y» and, for each i, Y**^. By 
contraction of the subexpression Y of A Q {Y} we have A {Y}»A {Y«}; since 
Y* is in normal form, the beta contraction of the redex P* in A Q {Y»} 

((LAMBDA(X)M{X)) Y» ) 

yields a contracture M{Y*} containing j instances of Y». But each 
instance of Y* may be contracted to the corresponding Y^, hence 
A () {Y»}»A 1 «. Then we have A () {Y}»A {Y*}»A 1 »»A nI and A Q »A n in R-*. 

The simplest illustration of the use of "-conversion to mitigate the beta-R 
restriction involves the evaluation of the expression A given by 

A = ((LAMBDA(X)3) B) 

5.1.3 -Q1- 


B = ((LAMBDA(H)(H H) )(LAMBDA<H) (H H)) 
■ince B has no normal form in the conventional lambda calculus (or, as a 
consequence, in Either-R) the beta-redex A cannot be contracted under beta-R. 
Hence A has no normal form in Either-R; in R-*, however, •-contraction on the 
subexpression B of A yields 

A > (<LAMBDA<X) 3) •) 
which may be contracted, under beta-R, to the value 3. We thus can derive the 
value 3 from the expression A, despite the restriction on beta conversion. We 
may of course derive other normal form values of A which involve the element 
*; these may be interpreted as "approximations" of the value of A in the sense 
that they retain partial information concerning the value of A. In this light 
the expression • itseOLf is a particularly bad approximation of A, as it gives 
no clue about the value of A. The expression 3 (which is, significantly, 
*-free) i.s a perfect approximation of A since it contains all of the 
information necessary to .-.derive the value of A — i.e,, A=3 in the lambda 

5.1.4: Consistency of R-* Theories 

We observe, at this point, that the addition of the *-conversion axiom to the 
lambda calculus does not lead to inconsistency; specifically, if X and Y are 
•free and X>Y in an R-* Theory, then X=Y in the corresponding Lambda 
calculus. The intuitive justification for this claim stems from the 
unidirectional nature of "-contraction - there is no corresponding abstraction 
operation. Thus if the reduction X»Y involves the *-contraction of a 
subexpression U, then U must be cancelled since Y is *-free. 

The consistency of the R-* Theories follows as' a special case of the 
consistency of the Either-R-* Theories, which is proved in the next chapter; 
consequently no proof is given here. 

5.2: Applications to the Lambda Calculus 

-92- 5.2 

The theorems of this chapter may provide tools of general usefulness in the 
study of the conventional lambda calculus. Suppose, for example, that neither 
of the expressions X and Y have normal forms in the beta-delta calculus, and 
that furthermore they are not interconvertible. He may still suspect, 
however, that they are equivalent in an extensional sense. In particular we 
may wish to prove that if either of Z{X} or Z{Y} has a normal form in the 
lambda calculus then Z{X}=Z{Y}. 

The mechanism of "-conversion suggests a technique for constructing such 
proofs. Suppose we could show that in R-* the expressions X and Y have 
identical sets of normal forms. 1 From Theorem 5. t1 it then follows that, for 
a^iy Z and every Z* in normal form, Z{X}»Z* if and only if Z{Y}»Z«. But 
Theorem 5.12 extends this extensional equivalence to th£ lambda calculus; 
hence for any Z and any normal form Z», Z{X}->Z» if and only if Z{Y}->Z* where 
-> denotes lambda calculus reduction. We deduce from these observations that 
any two expressions which have interconvertible sets of normal forms are 
eqivalent in this important extensional sense. 

We may apply, for sake of illustration, the above technique to the example 
cited by Scott 2 of the two fixed point operators 



Y t =(Y (LAMBDA(Y)(LAMBDA(G)(G (Y G))))) 

where Z is the expression 

(LAMBDA(H)(F (H H))) 

Y and Y 1 are not interconvertible in the lambda calculus, and neither has a 
normal form. Noting that Y contains the single redex (Z Z), the unique 
single contraction which can be made reduces Y Q to the expression 

(LAMBDA(F)(F (Z Z))) 

1 Specifically, we must show only that X»X» implies Y>Y»»X« and conversely, 
where X* and i* are any normal form expressions. 

2 Scott[22] credits the example to Corrado Boehm, and acknowledges an 
unpublished proof due to David Park that the expressions Y n and Y 1 are 
equivalent in the Scott formalism. u 

5.2 -93- 

which again contains the single redex (Z Z). It becomes clear from the 
sequence of reductions that this process leads to the conclusion that the 
normal forms (in R-») of Y are all of the form 

(LAMBDA(F)(F (F (F (F ... (F ») ... ))))) 

and for every natural number n there is a normal form Y » n whose body is F 
applied to • n times. 

We now refer to the definition of I... By Theorem 5.11, for every normal form 
Y^ of Y^Yq} there is a normal form Y Q » such that Y 1 {Y Q «}»Y 1 '. Hence every 
normal form of Y. is a normal form of Y^Yq*"} for some for some n. But each 
of the latter is of the form 

(G (G (G (G ... (G *) ... )))) 

where G stands for the expression (LAMBDA(Y) (LAIffiDA(G) (Y G))). But (G «) 
reduces to (LAMBDA(G)(G <• G))) from which, by contraction Of its »-redex, we 
arrive at Y •1=.(LAM8DA(G)(G *)). Then Y^sXG I «1) has as its maximal normal 
form (LAMBDA<G)(G XG •))); and it becomes clear from this informal argument 
that each R-* normal ibrm Y • n of Y 1 is of the form 

<LAMBM{G)(G <G <G <G ... (G *) ... ))))) 

whose body contains n applications of G. Thus each normal form derivable from 
Y_ in R- 1 is derivable from Y.., and conversely. 

Now if, for some X, X{Y-}=X* in the lambda calculus where X» is in normal 
form, then by Theorem 5.12 X{Y Q }>X* in R-». Then by Theorem 5.11 there is a 
normal form Y » n of Y Q such that X{Y Q « n }>>X»; since Y 1 has a normal form 
Y 1 * m »Y () » n , then XfY^^X* hence XM^sX* by the consistency of R-*. An 
entirely symmetric argument shows that X{Y..}=X* implies X{Y„}=X*. 

5.3: Summary 

The mechanism of *-conversion introduced in this chapter allows expressions to 
be approximated, to arbitrary accuracy, by expressions in normal form. The 
initial motivation for ^-conversion is the mitigation of the limitations on 
expressive power imposed by the restricted beta-conversion, but the techniques 

-94- 5.3 

of this chapter may be useful generally in the lambda calculus. 
The principal technical results of the chapter are: 

1) The introduction of • as a canonical representation of the undefined 
(nonterminating) computation, and the axiom on star conversion asserting 
that, for every X, X»». This axiom is motivated by the interpretation of 
> as denoting set theoretic inclusion in F*; the empty set, corresponding 
to the undefined computation •, is a subset of every element of F». 

2) Theorem 5.9 and its corollary establish that for any set A «...A » of 

1 * " n 
normal forms derivable from an expression A. in R-*, there exists an 

expression A* in normal form such that A»A* and A«>Ai for each i<n. 

3) Theorem 5.11 shows that if expression X{Y} is reducible to Z* , a normal 
form in R-*, then there exists a normal form Y» such that Y»Y* and 
X{Y«}»Z*. Informally this result assures us that, for every expression Y 
and every context X{Y}, there is a sufficiently good normal form 
approximation Y» of Y. The previous result (2)then guarantees that, for 
any finite set of approximations of Y, we can find a normal form Y* 
which may be used in lieu of any member of the set. 

*») Theorem 5.12 provides the final tie to the lambda calculus, by showing 
that every normal form derivable in the lambda calculus is derivable in 

The R-* Theory is thus as powerful, in an important sense, as the lambda 
calculus with unrestricted beta conversion. Furthermore, the R-* Theories 
suggest a natural test for extensional equivalence of expressions: the 
interconvertabillty of normal forms. This technique is applicable to the 
lambda calculus, and the extensional equivalence of noneonvertible fixed point 
operators Y Q and Y. is used as an illustration. 

The development of •-conversion in Chapter 5 is independent of the EITHER 
reduction of the previous chapter. The combination of the two mechanisms is 
the project of the next chapter. 

6 -95- 

Chapter 6: 
The Either-R-» Theories 

The desire for a syntactic basis for a language E, incorporating the EITHER 
mechanism informally described in Chapter 3, has led to the presentation (in 
Chapter 4) of the Either-R theory. It was noted that the restricted beta 
conversion of Either-R limits the usefulness of that theory since, for 
example, it prohibits the expression of recursive functions. The inadequacy 
of Either-R as a basis for the language E motivated the development, in the 
last chapter, of •-conversion. The present chapter brings these efforts to 
fruition in the form of the Either-R-» system, whioh consistently combines 
•-conversion with EITHER reduction and provides a satisfactory basis for a 
language E. 

Specifically, an Either-R-* theory shall consist of the following axioms, each 
of which is presented in a previous chapter: 

alpha. (Ch. 4) interconvertability (by renaming) of congruent expressions — 

e.g. (LAMBDA(X)X) • (LAMBDA(Y)Y) ; 
beta-R (Ch. 4) lambda conversion restricted to redexes whose arguments are 

in normal form — e.g. ((LAMBDA(X)X) 3)»3; 
various delta axioms (Ch. 4) specifying the interpretation of primitive 

functions and constants — e.g., (PLUS 3 5) • 8; 
epsj-lop (Ch. 4) contraction of E-redexes— e.g., (EITHER A B)>B (Ch. 4); 
lit (Ch. 4), abstraction of E-redexes — e.g. E«(EITHER E E); 
rho. (Ch. 4), distribution of function application over terms of an E-redex 

— e.g. (F (EITHER A B) )- (EITHER (F A) (F B)). 
fiigffla (Ch. 5) •-contraction — A>* for every expresion A. 

6.1: Consistency of Either-R-» 

The consistency of Either-R-« may be established by techniques closely 
analogous to the Either-R consistency proof. Recall that the earlier proof 
involved the notion of enclosure, and culminated in the implication of 
enclosure by > —i.e., X>Y in Either-R implies X encloses Y. Extension of 

-96- 6.1 

this technique to the present case requires that the mechanism of 
"-contraction be accounted for; accordingly, we extend the notion of 
enclosure by 

Defn 6.1: X " -encloses Y if, for each e-residue 1 Y' of Y, there exists an 
e-residue X' of X and an expression X* derived from X by •-contraction 
alone, such that X*=Y* in the lambda calculus. 

Note that we admit expressions containing the element * in the lambda 
calculus, treating * simply as a free variable. It is clear from the above 
definition that •-enclosure is transitive, and that if X encloses Y then X 
•-encloses Y. 

The following Lemma and its Corollary confirm that- •-contraction introduces no 
new equivalences in the conventional lambda calculus: 

Lemma 6.2: Let X and Y be •- and EITHER-free expressions, and let X>X« by the 
•-contraction of a subexpression U of X. If X # =Y in the lambda calculus, 
then X=Y. 

proof : Noting that X» contains a single • (the contractum of U), treating • 
as a variable in the lambda calculus gives us 

X=( (LAMBDA (»)X«) 0) 

by beta conversion. But X*=Y, hence 

Xr( (LAMBDA (•)Y) U) 

and as Y is f -free the contractum of this beta-redex is simply Y. Hence 

Corollary 6.3: If X and Y are «- and EITHER-free and X»X« by a series of 
•-contractions, then X*=Y in the lambda calculus implies X=Y. 

P»"QQf is by a simple induction on the number of •-contractions in the 

1 Recall Defn 4.7. 

6.1 _ 9 7- 

reduction sequence from X to X«. 

The above lemma and its corollary are hardly counterintuitive in light of the 
developments of Chapter 5. In particular, it is clear that any occurence of « 
in X* must be cancelled in the derivation of Y from X, since Y is »-free. 
Hence we may replace such occurences by arbitrary expressions, which are still 
cancelled in the derivation of Y; the choice of the homologous subexpressions 
of X yields X=Y. 

The consistency proof for Either-R-« follows the format of the corresponding 
proof for Either-R, except that the enclosure relation in the latter proof is 
extended to •-enclosure in the former. The basis of this extension is given 

Lemma 6.4: Let X>Y be a single reduction step in Either-R-«. Then X 
•-encloses Y. 

Proof : Lemma 4.13 establishes the lemma for the reductions allowed in 

Either-R; hence we need consider only the case of a •-contraction. Let 
U be the contracted subexpression of X. For each e-residue Y' of Y, 
there is a corresponding e-residue X' of X such that either X' and Y' are 
identical or Y' is the result of the *-contraction of an e-residue U' of 
U in X'. Hence X'»Y' by '-contraction, and X •-encloses Y. 

The following theorem is the Either-R-» analogy of Theorem 4.15: 

Thm 6.5: Let X and Y be expressions containing no occurrences of EITHER or «, 
and let X»Y in Eitlier-R-». Then X=Y in the lambda calculus. 

proof : By Lemma 6.4 and the transitivity of •-enclosure, X '-encloses Y. 
Since each of the expressions X and Y is EITHER-free, each expression is 
its own unique e-residue, and X»X*=Y where X>X» by •-contraction alone. 
By Corollary 6.3, X=Y in the lambda calculus. 

Thus the consistency of Either-R-* follows from the consistency of the lambda 

-98- 6.2 

6.2: Relation of « to EITHER 

We have already noted that the mechanism of '-contraction leads to the 
interpretation of each expression A as the upper bound, in the sense of >, of 
a family of expressions derivable from A. To formalize the relation between 
such a family of expressions, we introduce the terminology of 

Defn 6.6: Expressions X and Y are consistent in a theory T if and only if 
there is an expression Z such that both Z>X and Z>Y in T. 

Then the R-» theories are partitioned by the consistency relation into 
equivalence classes, of which there are infinitely many (since there are 
infinitely many mutually incongruent normal forms). Then the characteristic 
of R-* which is established by Corollary 5.10 is that any finite set of 
consistent expressions in normal form has an upper bound which is also in 
normal form. 

We note that in R-» the > ordering on the set of expressions derivable from an 
expression A is, in general, nontrivial. Unless A is the element * the upper 
bound of the set, A, is distinct from the lower bound *; furthermore there may 
be infinitely many expressions A^A.,*... in the set such that for no j>i is 
A >k . This is certainly not the case in the conventional lambda calculus, in 
which consistency implies interconvertibility and hence equivalence. What the 
mechanism of '-contraction has added to the lambda calculus is a method of 
deriving from an expression A an approximation A» to A which is strictly 
weaker in the sense of >. We may. then view the * mechanism as a method of 
introducing new expressions which are weaker than the conventional lambda 
calculus expressions, as each expression in R-* is derivable from a •-free 

In this light we must regard the EITHER construct as a mechanism for 
introducing stronger expressions into the lambda calculus. While R-» (and for 
that matter the conventional lambda calculus) contain upper bounds only for 
consistent sets of expressions, we can with EITHER represent the upper bounds 
of arbitrary (enumerable) sets of expressions. Observe further that, for 

1 Or, equivalently, we may say that in the Either theories, every set of 
expressions is consistent. 

6.2 -99- 

arbitrary expressions X and Y, the expression (EITHER X Y) is the least upper 
bound of X and Y since by Theorem 4.4, Z>X and Z>Y implies ZXEITHER X Y). 
This suggests that the ordering of Either-R-* expressions by > forms a 
complete lattice. 

6.3: Evaluators for E 

As we have noted, interpreters for languages supporting the EITHER construct 
require a slightly different structure from our previous examples: the 
reducibility of expressions to multiple values suggests that an evaluator for 
E should enumerate the values of the input expression. Accordingly, we 
formulate the evaluator as a function E of 2 arguments, an expression X to be 
evaluated and a numeric index j specifying which value is to be returned. The 
evaluator is constructed such that, for each X and j, E[X;j] is an expression 
X' in normal form such that X»>X' in Either-^*. The value of E[X;j] is, in 
general, not defined for all values of j; it may be assumed in particular 
that EEX;j] is undefined for those cases of X and j not represented in the 
algorithm presented informally below. We again assume the existence of an 
invertable pairing function, and use here the notation <n;m> to denote that 
natural number which uniquely encodes the ordered pair of natural numbers 
(n,m). We make the further assumption that for no n and m is <n;m><2. 

E[X;j] = 

if j=0 then •; 

if X is atomic and j=1 then X? 

if X is of the form (LAMBDA(Y)M) then (LAMBDA(Y)E[M;n] ); 
if X is of the form (EITHER A B) and j=<1;n> then E[A;n]; , 2 
if X is of the form (EITHER A B) and j=<2;n> then E[B;n]j 
if X is of the form (A B) and j =<<m;n>;p> then 
APPLY[E[ A;mj ;E[B;n] ;p] ; 

where the algorithm for APPLY is given informlly by 

APPLY[F;X;j] = 

Recall that the atomic expressions are identifiers (including primitive 
function symbols and variables) and numeric constants. 

-100- 6.3 

if F is of the form (LAMBDA(Y)M) then E[S[X;Y;M] ; j] ; 
if (F X) is a delta-redex and j=1 then F[X]; 
else if j=1 then (F X); 

We note that E[X;j] is in normal form where it exists, and the value E[X;j] is 
in each case the result of an Either-R-* contraction sequence on X. Although 
we don't claim that the values E[X;j] of X are ordered by > for successively 
higher values of j, the index j specifies, roughly, which of the 
approximations of X is to be returned. 

We may envision implementations of the E interpreter which make use of massive 
parallelism to compute simultaneously the values of (F X) for many different 
approximations of X; such use of redundant computation may serve to minimize 
the real time required to compute an acceptable value for X. Such an 
implementation follows, roughly, the spirit of fast adder circuitry which 
computes redundantly the high order portion of a sum simultaneously with the 
low order portion, and then selects the correct high order- portion on the ' 
basis of some intermediate carry. These implementational issues are largely 
ignored in the present work, but present some intriguing possibilities for 
future research. 

6.4: Summary 

The Either-R-* Theory may be used as the semantic basis for a language, E, 
which solves the specific expressibility problem demonstrated in Chapter 4. 
The evaluation of expressions in E lends itself naturally to the use of 
multiprocessing techniques which tend to minimize the total real time 
necessary to relize an acceptable evaluation of an expression (F X) by the 
simultaneous application of F to one approximation of X while computing a 
better approximation. While the implementation details are not pursued here, 
we feel that current technological developments make this area worthy of 
further study. 

7 -101- 

Chapter 7: 
The Either-K Theories 

The inconsistency of EITHER distribution (Axiom rho) with the unrestricted 
beta conversion of the lambda calculus has motivated the restricted beta-R 
conversion of the systems presented thus far. This chapter explores an 
alternative formulation, in which EITHER distributivity is sacrificed in order 
to accommodate the conventional (unrestricted) beta conversion. 

The Either-K theories include the axioms alpha, delta, epsilon, mu, and the 
(unrestricted) beta axiom of the lambda calculi: 

Axiom beta : Let E be an expression of the form ( (LAMBPA(a_>b_)c_). Then E«E', 
where E' is the contractum S[cja.;.bJ . 

Since Either-K preserves the axioms of the lambda calculi, it is clear that 
the equivalence • in Either-K is a proper extension of the lambda calculus 
equivalence =. In this sense the Either-K calculi are closer to the 
conventional lambda calculi than the Either-R-* theories. 

There is, however, a fundamental sense in which Either-K is a more radical 
departure from the lambda calculi than is Either^Rr*. In the latter theories 
functions are ultimately applied only to normal form operands whose semantics 
are those of the lambda calculi. The ability, in Either-K, to apply functions 
to multivalued expressions (such as E-redexes) requires that we reinterpret 
the semantics of each function relative to these new elements of its domain. 

7.1: K -abstraction 

By the axiom beta of the lambda calculus, the expressions 



((LAMBDA(x) M) A) 

are equivalent when A is an arbitrary expression and M contains no free 

S is the lambda calculus substitution function given in Defn 2.6. 

-102- 7- 1 

occurrences of the variable x. This fact is consistent with the observation 
that the bound variable, x, is ignored in the body of the function applied to 
A; hence the value of the application is independent of the value of the 
argument A. Despite the intuitive satisfaction with which we accept the above 
equivalence, the presence of functions which ignore their arguments 
complicates the proof of many otherwise straightforward results in the lambda 
calculus. Indeed, Church has argued against the inclusion of such functions 
in his theories, fearing at one time that they led to inconsistencies. 

The task of proving the consistency of the Either-K theories, to be attacked 
presently, is likewise complicated by the inclusion of functions which ignore 
their arguments. The definitions and results of this section provide the 
mechanism for dealing with the formation of such functions in later proofs. 
He begin with 

Defn 7.1: A K-redex is an expression of the form 

((LAMBDA(x)M) A) 

where A is any expression and M is an expression not containing free 
occurrences of the variable x. 

Defn 7.2: A K-abstraction is a reduction step* consisting of the replacement 

of a subexpression M by a K-redex of the form 

((LAMBDA(x)M) A) 

where A is any expression and x is a variable not occurring free in M. 

We now wish to show that the K-abs tract ions in a reduction sequence can be 
postponed to the end of the sequence. We introduce a term to describe 
reduction sequences whose K-abs tractions follow all other reductions: 

Defn 7.3: A reduction sequence R is K-normal if no K-abstraction in R 

1 For discussion and historical insight, see Curry[12], particularly the 
comment at the end of Ch. 3. 

2 recall Defn 4.1. 

7.1 -103- 

precedes a reduction step which is not a K-abs tract ion. 

Thus a reduction sequence X (J >x 1 >...M n is K_normal if there is an i , where 

Q<i<n, such that the reductions X Q >...X i are not K-abs tract ions and the 

reductions X. >...>X^ are only K-abs tract ions. We wish to show that, for every 
in ' 

reduction sequence X_>. . .>X, there exists a K-normal reduction sequence from 
X to X . We begin with sequences of length 1: 

Thm l.k: Let X-^X^X- be a two-step reduction sequence from X Q to X-, where 
the reduction step X >X. is a K-abstraction and the reduction step X->Xp 
is not a K-abstraction. Then there is a K-normal reduction sequence from 
Xq to X_j containing at most one reduction step which is not a 

proof : Let U be the subexpression of X which is replaced in the reduction 
step X >X.. Then U is replaced in this step by 0', an expression of the 

(<LAMBDA(y)U) A) 

where y is a variable not occurring free in 0. We exhaustively examine 
classes of the reduction step X 1 >X ? : 

Case 1: The reduction step modifies only the subexpression A of U'; let U 
become A' in X ? . The K-normal sequence from X. to X, is then the single 
K-abstraction replacing U by 

< (LAMBDA (y)U) A') 

Case 2: The reduction step modifies only the subexpression of U'; then U 
becomes W in X 2 . The K-normal sequence from X Q to X~ is then: 

a) Replace U in X Q by W, yielding X '; 

b) Replace W in X Q ' by the K-redex 

((LAMBDA(y)W) A) 
yielding J.^ 

Case 3: The expression U' in X 1 is replaced by U by beta reduction. Then 
X and X are identical expressions, and the empty reduction sequence 

-104- 7.1 

yields X- from X Q . 

Case 4: The reduction step replaces some subexpression V of X 1 by the 
expression V', where V is not a subexpression of U' and U' is not a 
subexpression of V. The K-normal sequence from X to X_ is then 

a) The replacement of V in X by V, yielding X '; 

b) The replacement of U in X ' by U', yielding X_. 

Case 5: The expression U' is replaced by the expression 


The K-normal sequence from X to X_ is then 

a) The replacement of U in X Q by (EITHER U U), yielding X Q '; 

b) The replacement of (EITHER U U) in X Q ' by (EITHER U' U') through two 
consecutive K-abs tract ions. 

Case 6: The expression U' is replaced by the expression 

(EITHER ((LAMBDA(y)U) A 1 ) ULA»fflBA(y)U) A ? ) 
by Axiom rho. The K-normal sequence from X. to X, is then 

a) The replacement of U in X Q by (EITHER U), yielding X Q '; 

b) The replacement of (EITHER U U) in X Q ' by 

(EITHER ((LAMBDA(y)U) A^ ((LAIfflDA(y)U) A 2 >) 
through two consecutive K-abs tract ions. 

Case 7: The subexpression U' is replaced by an expression W of the form 

((LAMBDA(z)U) A) 
derived from U' by alpha conversion. Then the variable z does not occur 
free in D, and X. may be reduoed to X_ by a single K-abs tract ion. 

Case 8: Some subexpression V containing U' is replaced by an expression 
V'. Then one of the following applies: 
8a) V' is derived from V by alpha conversion.. Then we may apply that 
alpha-conversion to X-, yielding X ', and follow with the 
K-abstraction from X ' to X ? . 
8b) V' contains n occurrences of 0', where n is zero or greater. Then 
there is a reduction of the same type from X_ to X Q ', where X ' is 
identical to X ? except for the n occurrences of in ■ X * corresponding 
to n occurrences of U' in X_. Our K-normal sequence from X Q to X_ 

7.1 -105- 

consists of the reduction of X to X ' followed by n K-abs tract ions 
replacing the occurrences of U by U'. 

This list of cases is exhaustive, completing the proof. 

Theorem 7.4 shows that every two-step sequence of reductions is equivalent to 
some K-normal reduction sequence. The generalization of this result to 
sequences of n reductions is complicated by the fact that the K-normal 
sequence guaranteed by Theorem 7.4 may be of arbitrary length, thus ruling out 
a simple induction on the length n of the reduction sequence. 

Lemma 7.5: Let R be a reduction sequence f ran X. to X containing exactly 1 

reduction step which is not a K-abs tract ion. Then there is a K-normal 

reduction sequence from L to X , 

v n 

proof : by induction on the length n of tile reduction sequence R. 

£Mis_: Trivially true for n<2} for n=2, guaranteed by Theorem 7.4. 

induction : Let X Q >X >.. ,>X be the reduction sequence R. If the step 

X Q >X 1 is not a K-abs tract ion, then R is K-normal; hence we may assume 

that X >Xv is a K-abs tract ion. Then a single step of the subsequence 

X >...>X is not a K-abs tract ion; by the inductive hypothesis, there is a 

K-normal reduction sequence X,>Y >Y >...« of which only the reduction 

step X,>Y Q may be other than a K-abs traction. But by Theorem 7.4, there 

is a K-normal sequence X «0>.,.>Y equivalent to the sequence X >X 1 >Y Q ; 

thus the reduction sequence X n «0>. ..>Y_>. ..« is K-normal fromX. to X . 

<* v n On 

t)efn 7.6: The K- index of a reduction sequence R is the number of 

non-K-abs tract ion steps in R which follow the first K-abstraction in R. 
If R contains no K-abs tractions, then the K-index of R is zero. 

Note that the K-index of a reduction sequence R is zero if and only if R is 
K-normal, We shall base the induction in the proof of the next theorem on the 
K-index of the reduction sequence to which it is applied. 

-106- 7.1 

Thm 7.7: Let R be a reduction sequence from X to X . Then there is a 
K-normal reduction sequence from X to X . 

proof is by induction on the K-index of R. 

basis ; If the K-index of R is zero, then R is K-normal. 

induction : The K-index n of R is greater than zero. Let X_>. . .>X denote 

u ft 

R, and let Xj^X^ be the first K-abstraetion in R. Let X,»X. j be the 
first reduction step following X^X^ in R which is not a K-abs tract ion; 
the existence of such a j is assured by the K-index of R. Then the 
subsequence X »X .j>. . ,>X « of R contains a single step which is not 
a K-abs tract ion; by Lemma 7.5 there is a K-normal sequence 
X >Y-». ..*X. - from X. to X. .. Then the sequence R" given by 
X Q >. . .>X.>Y_>. ..>X, ^2,. ..X has a K-index of n-t. By the induction 
hypothesis, there is a K-normal sequence from X. to X . 


It follows from Theorem 7.7 that every reduction sequence may be reordered in 
such a way that every K-abs tract ion follows every reduction step which is not 
a K-abs tract ion. Curry[12] refers to expressions as fictitious if they appear 
as the arguments of K-redexes; hence A is a fictitious subexpression of B if A 
is cancelled in the evaluation of B. Theorem 7.7 asserts that the 
introduction of fictitious subexpressions can be postponed to the end of a 
reduction sequence. Consider the following expressions: 

Z =. (LAhffiBA(X)3> 
A =. ((LAMBDA(H)(H H))(LAJffl»A(H){H H)) 
I =. (LAMBDA(X)X) 
Then the reduction sequence 

3 > (Z A) MI (Z A)) 
is not K-normal, since the K-abstraction 3>(Z A) precedes the beta abstraction 
(Z A»(I (Z A)). We may, however, reorder the sequence so that the fictitious 
subexpression A is introduced in the last reduction step; the resulting 
reduction sequence 

3 > (I 3) MI (Z A)) 
is K-normal. 

7.2 -107- 

7.2: Consistency of Either-K Theories 

It was noted, following the proof of the consistency of the Either-R theories, 
that the technique used there was inapplicable to the Either-K axioms since 
unrestricted beta conversion does not preserve the enclosure relation. We 
avoid this difficulty in the corresponding proof for the Either-K theories by 
arranging the reduction sequence of an EITHER-free expression so as to ensure 
that arguments in beta contractions are unitary. Since the Either-K reduction 
sequence of an EITHER-free expression can introduce non-unitary subexpressions 
only through K-abs tract ion, the result of the preceding section provides a 
critical step in the present proof. 

We begin by distinguishing expressions containing only unitary subexpressions: 

Defn 7.8: An expression X is pure if every subexpression of X, includitig X 
itself, is unitary. 

Note in. particular that every EITHER-free expression Is pure. We now precede 
to the major task of this section, which is the proof that the reductions 
permitted by our axioms preserve purity of expressions. We begin with the 
case of beta-contractions: 

Lemma 7.9: Let Y be EITHER-free and let X be a pure beta-redex of the form 

<(LAtfflDA(y)B) A) 

such that for each e-residue X' of X, X'=Y. If Z is the result of lambda 
conversion on X {ie, Z is the result of substituting A for each free y in 
B), then for every e-residue Z' of Z, Z'~Y. 

proof : Let Z' be an e-residue of Z. Then Z' contains zero or more 

occurrences of A p a 2 , ..., A n where each ^ is an e-residue of A. By 
the purity of X, A is unitary, hence each A. is convertible to Aj 
Z'=Z" where Z" is the result of lambda conversion on 

<(LA»fflDA(y)B') A^ 

where B' is some e-residue of B. Hence Z"=Y, and Z'=Y. 


-108- 7.2 

Lemma 7.10: Let X, Y, Z, and Z' be as in Lemma 7.9, above. Then Z is pure. 

proof : Let U be an arbitrary subexpression of Z, and let W be the 

corresponding subexpression of B. If W contains no occurrences of y 
which are free with respect to X, then W and U are identical, hence U is 
unitary by the purity of X. If H contains such occurrences of y, then U 
is the result of lambda conversion on 

((LAMBDA(y)H) A) 

and, by Lemma 7.9, U is unitary. 

We next show that beta abstractions preserve purity, so long as they are not 
K-a bs tract ions : 

Lemma 7.11: Let Z be a pure expression containing 1 or more occurrences of 
the subexpression A. Let W be a beta -red ex of the form 

( (LAMBDA (I )B) A) 

such that the contractum of W is Z. Then W is pure and, for every 
e-residue W' of W there exists an e-residue Z' of Z such that W'=Z'. 

proof : Since A is a subexpression of the pure expression Z, A is unitary; 
let the e-residues A ' A 2 ',...A. ' of A each be convertible to A' in the 
lambda calculus. For each e-residue B' of B there is a corresponding 
e-residue Z' of Z, such that Z' contains some A ' in place of each free 
occurrence of Y in B; hence Z'=S[A';y;B']. Each e-residue W is of the 

form ((LA i 'MBDA i '(Y)B')A i ') where B' is an e-residue of B; but then W is 
convertible to S[A';y;B']=Z'. Thus each e-residue W' of W is convertible 
to an e-residue Z' of Z. Noting that homologous subexpressions B1 and Z1 
of B and Z, respectively, are either identical or related by 
Z1=S[A';Y;B1], we deduce by the above argument and the purity of Z that B 
is pure. Hence W is pure. 

Note that Lemma 7.11 fails to hold for K-a bs tractions; consider, for example, 
the K-abs traction 

7.2 -109- 

M>( (LAMBDA (X)M) (EITHER 2 3)) 

where M contains no free occurrences of the variable X. Clearly the 
abstraction of M is impure regardless of the purity of M. We now present the 
principal result of this section, from which the consistency of the Either-R 
axioms follows directly: 

Lemma 7.12: Let X»Y be a single reduction step other than a K-abstraction in 
Either-K, and let X be pure. Then Y is pure and X encloses Y. 

proof: The cases where X»Y is a beta conversion follow directly from Lemmas 
7.9, 7.10, and 7.11; and if the step is an alpha conversion, the 
e-residues of Y are clearly congruent to the e-residues of X, and Y is 
pure. If X»Y is a delta conversion then both X and Y are EITHER-free and 
the lemma is trivially true. If X>Y is an EITHER-conversion in either 
direction, the purity of Y follows fr'm the purity of X and the 
e-residues of X and Y are identical. 

The consistency of the Either-K theories is presented as 

Thm 7.13: Let X and Y be EITHER-free expressions, and let X»Y in Either-K. 
Then X=Y in the lambda calculus. 

proof: From Theorem 7.7, we may assume that there is a K-normal reduction 
sequence from X to Y; let X>. ..M^T^. . .>Y be such a sequence, where the 
subsequence X»...>Y Q contains no K-abs tract ions and Y >...>Y contains 
only K-abstractions. Then Y Q must be EITHEB-free, since each of the 
K-abs tractions Y^Y^ can only increase the number of EITHER redexes, 
and Y is EITHER-free. Y q= y in the lambda calculus since each of the 
conversions Y Q >...>Y is a valid beta conversion. By Lemma 7.12, X must 
enclose Y Q since X is pure; but each of these expressions is EITHER-free 
and hence is its own e-residue. Thus X=Y.=Y. 

Corollary 7.14: Let X and Y be EITHER-free expressions, and let X-Y in 
Either-K. Then X=Y in the lambda calculus. 

-110- 7.2 

Proof : Directly from Corollary 7.13. 

7.3: Functional Domains of Either-K 

The semantics of the Either-K Theories bear a superficial similarity to those 
of the corresponding Either-R-« Theories: in each case a functional domain F 
of the lambda calculus is extended to a domain F* whose elements are 
enumerable subsets of F. The question of restrictions on beta conversion 
seems, at first glance, to be an issue of evaluation order whose semantic 
ramifications parallel, say, those of the applicative /normal order 
distinction. While this analogy can be defended, as it has been in earlier 
sections of this thesis, there is evidence suggesting that the distinction 
between the Either-R and Either-K semantics is of a rather more fundamental 

The distributivity of function application over EITHER terms, sanctioned in 
the Either-R Theories by Axiom rho, constitutes a limitation on the expressive 
power of languages built on these theories. Consider, for example, the 
function f whose informal definition is 

f[x] = x+x; 

which computes, in the lambda calculus, a numeric value which is twice the 
value of its argument x. Our experience with conventional applicative 
languages reinforces an intuitive expectation that f will have only even 
numbers in its range (assuming that the domain of f is the set of natural 
numbers). The natural extension of our intuition to the Either-R Theories is 
consistent with the range of f there,, containing enumerable sets of even 
numbers. In the Either-K Theories, however, we must realign our intuition. 
The application of f to the argument eitherE2;3l, for example, is reducible in 
Either-K to any of the numbers in {4,5,6} rather than the {4,6} result of 
Either-R. Thus although the semantics of the application of functions to 
single-valued arguments remains consistent with the lambda calculus, the 
behavior of functions with multivalued arguments differs between the Either-R 
and Either-K systems. 

7.3 -111- 

A more bizarre demonstration of this difference is the function g. defined 
informally by 

g[x] = if x >x then 1; 
else 0; 

which, in the lambda and Either-R calculi is equivalent to the single argument 
constant function which always returns zero. Yet the Either-K reduction of 
g[either[1;2]] yields the values {0,1}, even though g[1] and g[2] each 
evaluate to {0}. Since the behavior of g in Either-K violates the 
distributivity axiom of the Either-R Theories, we clearly cannot express in 
these theories a function with the properties of g; yet g appears to be a 
computable function definable on the domain F*. 

7.4: Summary 

This chapter presents a consistent theory which combines EITHER conversion 
with unrestricted beta conversion. This combination requires 1) that we 
abandon the distributivity of functions over EITHER terms, and 2) that we 
reinterpret the semantics of EITHER. The latter reinterpretation is only 
hinted at in this chapter, and we confess that the semantics of the Either-K 
theories require further study. 

This empty page was substituted for a 
blank page in the original document. 

8 -113- 

Chapter 8: 
Summary and Conclusions 

There has been a definite tendency, in the course of the work reported here, 
to provide questions much more frequently than answers. We regard this 
situation, perhaps 'defensively, as a healthy attribute of research in a field 
as theoretically immature as the science of programming languages. 

8.1: Summary 

The general topic of this thesis is the correspondence between the syntactic 
mechanism of an interpreter and the semantic structure of the language it 
interprets. The restriction of this study to the class of applicative 
languages is defended, in Chapter 1, on the grounds that 

i) Interpretive mechanism for applicative languages is simple, since such 
complications as assignment, side effects, and transfers of eontrol are 
ii) The semantics of applicative languages are independent of the notion of 

iii) The theories of mathematical functions may serve as a semantic basis 

for applicative languages. 

Expressions of an applicative language are viewed as representations of 
objects in an abstract semantid functional domain containing functions and 
constants, and expressions are semantically equivalent if they represent the 
same abstract element. 

The stack- and tree-environment interpreters presented in Chapter 2 illustrate 
semantic limitations imposed by typical compromises between efficiency and 
expressive power. The defect of S must be viewed as an interpreter "bug" if 
we take mathematical functions as a semantic basis, since certain expressions 
are interpreted by S in a manner inconsistent with the behavior of functions. 

The T interpreter of Chapter 2 relates the issue of evaluation order to the 
expressibility of certain functions. The applicative order evaluation of T, 

i.e., the FUNARG problem. 

-114- 8 - 1 

in which arguments to a function are evaluated before the application of the 
function, is seen to lead to the inexpressibility of functions which ignore 
the value of their arguments. This motivates a preference for the normal 
order evaluation of the N model, in which such functions are expressible. The 
demonstration in chapter 2 of a functional domain F of N assures us that every 
expression is interpreted by N in a way that is consistent with our functional 
semantics; it does not, however, establish that every valid semantic element 
(e.g. , every computable function defined on the semantic domain of N) is 
expressible in N, 

Chapter 3 demonstrates a function, WHICHFF, which despite its computability is 
expressible neither in N nor in the lambda calculus. The expressibllity of 
WHICHFF seems to require a mechanism analogous to multiprocessing, and two 
therapeutic language extensions are considered: 

i) A "coding" primitive which allows a program access to the representation 
of a function supplied as its argument; and 

ii) A primitive EITHER whose interpretation involves the dovetailed 
evaluation of its arguments. 
The admission of coding essentially abandons all semantic constraints and 
allows the programmer to reinterpret expressions as he wishes; we thus discard 
this alternative as semantic anarchy. The EITHER primitive may be justified 
in terms of applicative semantics, however, by the expansion of the semantic 
domain F into the power set F* , each of whose elements is a subset of F. Thus 
once EITHER is introduced we must semantical ly associate each expression X 
with an enumerable set of abstract values or "meanings* of X. Such a 
multivalued semantic domain is necessary to reconcile the function WHICHFF 
with applicative language semantics. 

The semantic domain F* motivated in Chapter 3 is suggestive of a complete 
lattice ordered by set theoretic inclusion. The undefined (or nonterminating) 
computation is naturally associated with the empty set in F*, and that 
expression TOP whose values include the entire domain of the lambda calculus 
corresponds to the maximal element of F». The semantic element associated 
with the expression either[a;b] becomes the union of the respective F* 
elements corresponding to the expressions a and b. 

8.1 -1 15- 

In Chapter 4 our attention returns to the subject of interpretive mechanisms. 
In particular we desire a formalism for syntactic manipulation of expressions 
in a language including EITHER, reflecting the insight gained through informal 
scrutiny of the structure of F« in Chapter 3. The formalisms introduced in 
Chapters 4-7 are systems of conversion axioms, similar to (and based on) the 
lambda calculus; each system (or theory) defines an ordering, >, corresponding 
to inclusion in F» — thus, for example, either[a;b]>a and either [a ;b]»b in 
each system. 

A complication arising in Chapter 4 involves the reconciliation of the beta 
reduction of the lambda calculus with the intuitively motivated requirement 
that functions be distributive over EITHER terms — i.e., that f [either[a;b] ] 
be equivalent to either[f[a] ;f[b]]. The EITHER-R system presented in Chapter 
4 resolves this difficulty by restricting beta conversion to arguments which 
are reduced to normal form; while consistent, the resulting theory is too weak 
to be useful. 

The syntactic mechanism of *-conversion, presented in Chapter 5, solves this 
problem of Either-R. Chapter 5 introduces the expression * as a canonical 
(normal form) representation of the undefined computation, and extends the 
ordering > so that the syntactic significance of * (k>* for every expression 
A) reflects the semantic significance of the undefined computation (the empty 
set is a subset of every element of F»). The use of '-reduction allows every 
expression, including the single-valued expressions of the conventional lambda 
calculus, to be reduced to multiple normal forms. The R-* theory developed in 
Chapter 5 reinforces an interpretation of the normal forms derivable from an 
expression X as approximations to X, and shows that for any context A{X} 
having normal form value A' there exists a sufficiently good (normal form) 
approximation X* of X such that A{X»} also has the value A'. This result has 
major semantic consequences; in particular, it implies that meaning of an 
expression X is completely characterized by the set of normal forms derivable 
(in. R-») from X. Moreover the result is shown to carry over to the 
conventional lambda calculus, since every normal form derivable in the lambda 
calculus is derivable in R-*. The extensional semantic equivalence relation 

Informally, beta reduction is the application of a lambda expression 

thrh«1nS ^ir^?2 t fn n J^ y K^ bst ^ t ^ i0 ? °L its arguo?nt for free occurences of 
tne bound variable in the body of the lambda expression. 

-116- 8.1 

suggested by these findings, namely the interconvertability of normal forms 
derivable in R-*, is demonstrated by showing the equivalence of 
non-interconvertable expressions for the fixed point operator Y. 

The mechanisms of "-conversion and EITHER-reduction are combined, in Chapter 
6, to yield the Either-R-* system. The respective functions of the two 
mechanisms are, in a sense, complementary; roughly speaking EITHER allows 
expressions to be combined to make "stronger" expressions while "-conversion 
allows expressions to be resolved into weaker component expressions. The 
Either-R-* system is consistent, retains the power of the lambda calculus, and 
interprets EITHER according to the semantic notions of Chapter 3. We thus 
view Either-R-» as a practical syntactic basis for the construction of for 
interpreters of languages based on multivalued semantic domains; such an 
interpreter, E, is presented at the end of Chapter 6. 

Chapter 7 explores an alternative resolution of the conflict between 
unrestricted beta conversion and the distributivity of functions over EITHER 
terms. The Either-K system presented in that chapter sacrifices such 
distributivity in order to allow the unrestricted beta conversion of the 
lambda calculus. While this combination results in a consistent theory (as 
demonstrated in Chapter 7) it leads to a semantic structure which is 
fundamentally different from that of the Either-R theories, in particular 
regarding the application of functions to multivalued arguments. 

8.2: Conclusions 

The study of applicative languages from the complementary viewpoints of 
interpretive and semantic structure leads synergistically , we feel, to a new 
insight in each area. We have repeatedly found the syntactic mechanisms and 
semantic structures to be mutually illuminating, and view this dual 
perspective as a principal influence on the direction and motivation of this 

The following are viewed as the principal results of this thesis: 

1) The motivation and presentation of an applicative model of 

multiprocessing. The applicative approach to this mechanism has certain 

8.2 -117- 

technical advantages over conventional formulations; notable among these 
is the complete irrelevance of time as a parameter of language semantics. 
The corollary disadvantage of the applicative model is its uselessness in 
the study of time dependent implementation considerations — such as 
scheduling, deadlocks, and synchrony of processes. 

2) The formulation of the semantic domain F* for multivalued applicative 
languages. We find particularly interesting the potential extension of 
the Scott formalism which F* suggests: we have added, to the Scott 
domain, unique upper bounds of arbitrary sets of semantically distinct 
elements. The lack of such upper bounds in the Scott model has been 
conspicuous, and the EITHER construct presented here seems to provide a 
natural interpretation for them. 

3) The mechanism of *-conversion and the results relating it to the 
conventional lambda calculus. These results augment the lambda calculus 
with a syntactic substructure (i.e., the ordering under >) which bears 
close analogy to the semantic structure developed by Scott. In addition, 
•-conversion provides a concrete (syntactic) relation of semantic 
equivalence which may illuminate the relationship between lambda calculus 
expressions having no normal forms. 

4) The presentation of consistent theories of EITHER conversion. The 
analyses of these systems is by no means exhaustive; we have not shown, 
for example, that no axiom is derivable from the remaining axioms. The 
theories do, however, provide sufficiently powerful syntactic mechanism 
that interpreters may realistically be based upon them. 

8.3: Directions of Future Research 

We recognize that this section constitutes fertile grounds for an essay strewn 
with universal quantifiers. Restricting our attention to specific questions 
left unanswered by this work, we find most demanding of further attention: 

1) The relative expressive power of EITHER-augmented versus CODE-augmented 
( languages. We conjecture that every computable function defined on the 
single-valued domain of the lambda calculus is expressible in the 
language E, and have in fact spent considerable effort in trying 

-118- 8.3 

(unsuccessfully) to prove this conjecture. The discovery of computable 
functions expressible (with coding) in C but inexpressible (with EITHER) 
in E would be counterintuitive and somewhat depressing. 

2) The semantics and expressive power of languages based on the Either-K 
Theories. The presence of functions which compute different results for 
a multivalued argument X than for singlevalued components of X raises new 
fundamental questions: what is a computable function on F*? Are the 
Either-K Theories functionally complete? If not (and we are pessimistic 
on that issue) which functions are not expressible in Either-K?- 

3) There appears to be a great deal of room for further development of the 
theories of EITHER conversion. The extension of these theories to allow 
eta reduction seems feasible. Further extensions may make the 
extensional relation of semantic equivalence tractable by syntactic means 
alone, e.g. by axiomatically asserting in Either-R-* the equivalence of 
expressions whose normal forms are interconvertable. 

4) The area of interpretive mechanisms for EITHER-based languages has some 
interesting possibilities. The techniques of computational complexity 
studies, for example, might yield some quantitative bounds on the 
computation time necessary for the evaluation of classes of applicative 
expressions. As the cost of computation power continues to plummet, 
methods for making use of massive parallelism becomes a practical as well 
as academic interest. 

5) The relationship between the mechanisms of EITHER- and *-conversion and 
the semantic constructions of Scott demand more serious attention than 
the informal parallels drawn here. Much of Scott's important work seems 
to bear rather directly on the systems presented here, and we recognize 
that too little advantage has been taken of this resource. 

It must finally be acknowledged that our quest for a functionally complete 
language — one whose domain D contains every computable function defined on D 
— has not been an unqualified success. The lambda calculus, whose functional 
completeness was suspect, was scrutinized and found to be incapable of 
expressing certain functions (e.g. WHICHFF). To remedy this inadequacy, the 
lambda calculus was extended via the EITHER construct; the result (the Either 

8.3 -119- 

theories) is, indeed, capable of expressing WHICHFF. However, the new 
systems have additional elements in their domain, so that the functional 
completeness of the Either theories is again suspect. The results of this 
thesis, then, suggest a similar program of scrutiny and extension to repair 
their inadequacies. There is an inevitable circularity in this course of 
research, mitigated by the fact that each cycle allows us to see previous 
cycles more clearly. 

A way a lone a last a loved along the/ 
riverrun, past Eves and Adam s, from 
swerve of shore to bend of bay, brings 
us by a commodius vicus of recirculation 
back to Howthe Castle and Environs. 

-Finnegan's Hake, 
last/first lines 

-120- 9 


[I] Church, A.. The Calculi of Lambda Conversi o n . Annals of Mathematics 

St udi es, Princeton university Press 19 1 *! . 

[2] Landin, P, "A lambda -cal cuius Approach" In Advances in Programming and 
Non-numerical Computation. Peraagon Press, NewTork 19ob. 

[3] Dertouzos, M.. Structure and Interpretation of Computer Languages (class 

[4] Perils, A. J., "The Synthesis of Algorithmic Systems", JACM, January 1967. 
[5] ^.^ftgHl^flllJli^ Technical 

[6] Scott, D. , The La ttice of Floy Diagrams. Technical monograph PRG-3, Oxford 
University November 1970. 

[7] Hoare, C. A. R. , "Procedures and Parameters: An Axiomatic Approach". 
Lecture Rotes in Mathematics 188, Springer-Verlag, Berlin 1971. 

t8] ^"^t^C^^^HM^^W^f- 

[9] Cooper, D. C. , "Program Schemes, Programs and Logic". Lecture Notes in 
Mathematics 188. Springer-Verlag, Berlin, 1971. 

[10] Moses. J., "The Function of FUNCTION in LISP (or, Mhy the FUNARG Problem 
Should Be Called the Environment Problem)", SIGSAM Bulletin 15, July 

[II] Rosenblocn, P. C. , The |lementsof Mathematical Logic. Dover 

[12] Curry, H. B., and Feys, R. , Combinatory Logic. Amsterdam, 1958. 

[13] Paterson, M.S., "Program Schemata", Machine Intelligence III. Edinburgh 
University Press 1968. 

[14] Strachey. C. , "Fundamental Concepts in Programming Languages", NATO 
Conference, Copenhagen, 1967. 

[15] Morris, J., j^«hd«-nainul»s Mr^elg flf PrffffTgWlnff Languages. PhD Thesis, 

[16] Schwartz, J.T. , "Semantic Definition Methods and the Evolution of 

Programming Languages" in ESEMl Semantics St Pr»ff' , flTlBl I, P Languages, 
Prentice-Hall 1972. 

[17] Ershov, A.P. , "Theory of Program Schemata", IFIP Congress 71, August 

[18] Landin, P.J. , "The Next 700 Programming Languages", C ACM March 1966. 

[19] Wegner, P., "Programming Language Semantics", in Formal Semantics pf 
Prv T n ftffiff1nfr Languages. Prentice-Hall 1972. 

[20] Boehm, C. "Alcune Proprieta Delle Forme beta-eta -norma li nel 

lambda -K-calculo," Consiglio nazionale deile ricera Roma 696, 1968. 

[21] Hindley. J.R. et al, Introduction to Combinatory Logic. Cambridge 
UnlversityPress 1972. 

[22] Scott, D. "Lattice Theory, Data Types and Semantics" in Formal Semantics 
of Programming Languages. Prentice-Hall 1972. 


[23] Weizenbaum. J. "The FUNARG Problem Explained", unpublished memorandum, 
MIT 1968. 

[24] Walk, K. et al , "Abstract Syntax and Interpretation of PL/1, Version 
III," IBM Laboratory, Vienna TR25.098, 1969. 

[25] Floyd, R W. "Assigning Meanings to Programs," Proc. Symposium on Appl. 
Math, volume 19, 1967. 

[26] McCarthy, J. et al , The LISP 1.5 Programming Manual MIT Press 1965. 

[27] Curry, H. B. et al , Combinatory Logic vol. II, Amsterdam, 1972. 

This empty page was substituted for a 
blank page in the original document.